proposition: Lemma ext_prop_dep_proof_irrel_cc : prop_extensionality -> BoolP_dep_induction -> proof_irrelevance.
proof: Proof. exact (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl BoolP_elim_redr). Qed.
imports: PropExtensionalityFacts