proposition: Lemma base_paths_pair_path_in2 {X : UU} (P : X → UU) {x : X} {p q : P x} (e : p = q) : base_paths _ _ (pair_path_in2 P e) = idpath x.
proof: Proof. now induction e. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics