proposition: Lemma aux : prop_extensionality -> bool_dep_induction -> true = false.
proof: Proof. intros Ext Ind. case (ext_prop_fixpoint Ext bool true); intros G Gfix. set (neg := fun b:bool => bool_elim bool false true b). generalize (eq_refl (G neg)). pattern (G neg) at 1. apply Ind with (b := G neg); intro Heq. - rewrite (bool_elim_redl bool false true). change (true = neg true); rewrite Heq; apply Gfix. - rewrite (bool_elim_redr bool false true). change (neg false = false); rewrite Heq; symmetry ; apply Gfix. Qed.
imports: PropExtensionalityFacts