FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate
[~helmut/bidiragda.git] / Bidir.agda
index cbe693c..5587d20 100644 (file)
@@ -130,7 +130,7 @@ theorem-1 G {i} s = begin
       h′↦r (fromFunc f)
         ≡⟨ P.refl ⟩
       fmapS (flip lookupM (fromFunc f)) t
-        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩
+        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lookup∘tabulate (just ∘ f)) t ⟩
       fmapS (Maybe.just ∘ f) t
         ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩
       fmapS just (fmapS f t)