helm/matita/tests/apply.ma

   1 (* test _with_ the WHD on the apply argument *)
   2
   3 alias id "not" = "cic:/Coq/Init/Logic/not.con".
   4 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
   5
   6 theorem b:
   7   \forall x:Prop.
   8   (not x) \to x \to False.
   9 intros.
  10 apply H.
  11 assumption.
  12 qed.
  13
  14 (* test _without_ the WHD on the apply argument *)
  15
  16 alias symbol "eq" (instance 0) = "leibnitz's equality".
  17
  18 theorem a:
  19   \forall A:Set.
  20   \forall x,y : A.
  21   not (x=y) \to not (x=y).
  22 intros.
  23 apply H.
  24 qed.