Definition pair_path_in2_comp1 {X} (P:X->Type) {x:X} {p q:P x} (e:p = q) : maponpaths pr1 (maponpaths (tpair P _) e) = idpath x. Proof. intros. induction e. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.