]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/apply.ma
added Variant theorem flavour
[helm.git] / 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.