proposition: Lemma De_Morgan_nand_realizer : forall e, De_Morgan_nand↓e ⊩ ∀A B C, ((A ∧ B) → C) → ((A → C) ∨ (B → C)).
proof: Proof. do 4 Ksolve. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping