X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Funifhint.ma;h=310512b5a73003a332c028582837ed67e4cc95d9;hb=b97a7976503b2d2e5cbc9199f848135a324775a8;hp=42e9f687888ffd12ddf5cb9bdded6af59a35963d;hpb=c7605859c88549b8a812a19b85b3bbba53182ada;p=helm.git

diff --git a/helm/software/matita/tests/unifhint.ma b/helm/software/matita/tests/unifhint.ma
index 42e9f6878..310512b5a 100644
--- a/helm/software/matita/tests/unifhint.ma
+++ b/helm/software/matita/tests/unifhint.ma
@@ -88,6 +88,18 @@ unification hint 0 (∀g:group.∀G:list (gcarr g).∀x.
       〚x,G〛 = V).
 *)
 
+include "nat/plus.ma".
+unification hint 0 (∀x,y.S x + y = S (x + y)).
+
+axiom T : nat → Prop.
+axiom F : ∀n,k.T (S (n + k)) → Prop. 
+lemma diverge: ∀k,k1.∀h:T (? + k).F ? k1 h. 
+    ?+k    = S(?+k1)
+    S?1 + k   S(?1+k1)
+    
+lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
+   start g ? ? h.
+
 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
    start g ? ? h.