proposition: Lemma sigma_eq@{i} (A : Type@{i}) (P : A -> Type@{i}) (x y : sigma P) : x = y -> Σ p : (x.1 = y.1), transport p x.2 = y.2.
proof: Proof. intros H; destruct H. destruct x as [x px]. simpl. refine (id_refl, id_refl). Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes