proposition: Lemma invmap_eq {A B : UU} (f : A ≃ B) (b : B) (a : A) : b = f a → invmap f b = a.
proof: Proof. intro H. apply (invmaponpathsweq f). etrans. apply homotweqinvweq. apply H. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics