proposition: Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance.
proof: Proof. exact (fun pe => ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl boolP_elim_redr pe boolP_indd). Qed.
imports: PropExtensionalityFacts