proposition: Lemma path_prodE {A B : Type} {x x' : A} {y y' : B} : (x, y) = (x', y') -> x = x' /\ y = y'.
proof: Proof. move=> e; split; move: e. - by move=> /(ap fst). - by move=> /(ap snd). Defined.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy Param_nat