proposition: Lemma existT_eq_existT : forall (A:Type) (P:A->Prop) (x y:A) (p:P x) (q:P y), x = y -> existT P x p = existT P y q.
proof: Proof. Proof using. intros. rewrite (proof_irrelevance q (eq_rect x P p y H)). subst*. Qed.
imports: TLC(LibTactics LibAxioms)