helm/matita/tests/apply.ma

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