proposition: Corollary De_Morgan_nor_realizer_not : forall e, De_Morgan_nor↓e ⊩ ∀A B, ¬(A ∨ B) → (¬A ∧ ¬B).
proof: Proof. intro e. apply (sub_term (De_Morgan_nor_realizer e)). subtyping. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping