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