proposition: Lemma exist_eq_exist : forall (A:Type) (P : A->Prop) (x y : A) (p : P x) (q : P y), x = y -> exist P x p = exist 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)