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