shorten line length of theorem-1

1 files changed, 8 insertions, 6 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 853d70e..cc6f75f 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -168,19 +168,21 @@ theorem-1 get s = begin
     ≡⟨ cong (bff get s) (free-theorem get (denumerate s) (enumerate s)) ⟩
   bff get s (map (denumerate s) (get (enumerate s)))
     ≡⟨ refl ⟩
-  fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (denumerate s))) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s)))))
-    ≡⟨ cong (fmap (flip map (enumerate s) ∘ flip lookup) ∘ fmap (flip union (fromFunc (denumerate s)))) (lemma-1 (denumerate s) (get (enumerate s))) ⟩
-  fmap (flip map (enumerate s) ∘ flip lookup) (fmap (flip union (fromFunc (flip lookupVec s))) (just (restrict (denumerate s) (toList (get (enumerate s))))))
+  (h′↦r ∘ h↦h′) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s))))
+    ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩
+  (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s))))
     ≡⟨ refl ⟩
-  just ((flip map (enumerate s) ∘ flip lookup) (union (restrict (denumerate s) (toList (get (enumerate s)))) (fromFunc (denumerate s))))
-    ≡⟨ cong just (cong (flip map (enumerate s) ∘ flip lookup) (lemma-union-restrict (denumerate s) (toList (get (enumerate s))))) ⟩
-  just ((flip map (enumerate s) ∘ flip lookup) (fromFunc (denumerate s)))
+  (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (fromFunc (denumerate s)))
+    ≡⟨ cong (h′↦r ∘ just) (lemma-union-restrict (denumerate s) (toList (get (enumerate s)))) ⟩
+  (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
   just (map (flip lookup (fromFunc (denumerate s))) (enumerate s))
     ≡⟨ cong just (map-cong (lookup∘tabulate (denumerate s)) (enumerate s)) ⟩
   just (map (denumerate s) (enumerate s))
     ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
   just s ∎
+    where h↦h′ = fmap (flip union (fromFunc (denumerate s)))
+          h′↦r = fmap (flip map (enumerate s) ∘ flip lookupVec)
 
 lemma-fmap-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → fmap f ma ≡ just b → ∃ λ a → ma ≡ just a
 lemma-fmap-just {ma = just x}  fmap-f-ma≡just-b = x , refl