proposition: Lemma independence_general_premises_right_distr_implication_over_disjunction : IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction.
proof: Proof. intros IP A B C HCAB. destruct (IP bool (fun b => if b then A else B) C true) as ([|],H). - intro HC; destruct (HCAB HC); [exists true|exists false]; assumption. - left; assumption. - right; assumption. Qed.
imports: PropExtensionalityFacts Hurkens