fact: Definition not_all_ex_not_rel1 := λ"f" callcc @ (λ"g" ("f" @ (λ"r" callcc @ (λ"h" ("g" @ (λ"i" ("i" @ "r" @ "h"))))))).
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping