fact: Definition De_Morgan_nand := λ"nand" λ"nAZ" λ"nBZ" callcc @ λ"k" "nAZ" @ λ"a" "nand" @ (λ"f" callcc @ λ"k'" ("k" @ ("nBZ" @ λ"b" "k'" @ ("f" @ "a" @ "b")))).
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping