1 %% test _with_ the WHD on the apply argument
3 alias id "not" = "cic:/Coq/Init/Logic/not.con".
4 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
8 (not x) \to x \to False.
14 %% test _without_ the WHD on the apply argument
16 alias symbol "eq" (instance 0) = "leibnitz's equality".
21 not (x=y) \to not (x=y).