proposition: Lemma eq_rect_existT_eq: forall (X: Type) (P: X -> Type) (x1 x2: X) (H1: P x1) (H2: P x2) (Hx: x1 = x2) (Hex: existT P x1 H1 = existT P x2 H2), H2 = eq_rect _ P H1 _ Hx.
proof: Proof. intros; subst. subst; destruct_existT. reflexivity. Qed.
imports: Coq.Arith.Peano_dec Coq.Logic.Eqdep Coq.Logic.Eqdep_dec Coq.Program.Equality