proposition: Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction : GodelDummett <-> RightDistributivityImplicationOverDisjunction.
proof: Proof. split. - intros GD A B C HCAB. destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption. - intros Distr A B. destruct (Distr A B (A\/B)) as [HABA|HABB]. + intro HAB; exact HAB. + right; intro HB; apply HABA; right; assumption. + left; intro HA; apply HABB; left; assumption. Qed.
imports: PropExtensionalityFacts Hurkens