proposition: Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
proof: Proof. Proof proof_irrelevance_cci classic. Ltac classical_right := match goal with |- ?X \/ _ => (elim (classic X);intro;[left;trivial|right]) end. Ltac classical_left := match goal with |- _ \/ ?X => (elim (classic X);intro;[right;trivial|left]) end. Require Export EqdepFacts. Module Eq_rect_eq. Lemma eq_rect_eq : forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. intros; rewrite proof_irrelevance with (p1:=h) (p2:=eq_refl p); reflexivity. Qed.
imports: ClassicalFacts