proposition: Lemma ext_prop_dep_proof_irrel_gen : prop_extensionality -> bool_dep_induction -> proof_irrelevance.
proof: Proof. intros Ext Ind A a1 a2. set (f := fun b:bool => bool_elim A a1 a2 b). rewrite (bool_elim_redl A a1 a2). change (f true = a2). rewrite (bool_elim_redr A a1 a2). change (f true = f false). rewrite (aux Ext Ind). reflexivity. Qed.
imports: PropExtensionalityFacts