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