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. now induction e. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.