-unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g). 〚Eopp x,G〛 = (@〚x,G〛) ^-1).
-unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g). 〚Emult x y,G〛 = (@〚x,G〛) * (@〚y,G〛)).
-unification hint 0 (∀g:group.∀G:list (gcarr g). 〚Eunit,G〛 = 𝟙).
-unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g. 〚(Evar 0), (x :: G)〛 = @x).
-unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.(@〚Evar n, G〛)=
- (〚(Evar (S n)), (x :: G)〛) ) .
+
+unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g).
+
+ V1 ≟ 〚x,G〛 V2 ≟ 〚y,G〛
+(* ------------------------------------ *)
+ 〚Emult x y,G〛 = V1 * V2).
+
+unification hint 0 (∀g:group.∀G:list (gcarr g).
+
+(* ------------------------------------ *)
+ 〚Eunit,G〛 = 𝟙).
+
+unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g.
+
+ V ≟ x
+(* ------------------------------------ *)
+ 〚(Evar 0), (x :: G)〛 = V).
+
+unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.
+
+ V ≟ 〚Evar n, G〛
+(* ------------------------------------ *)
+ 〚(Evar (S n)), (x :: G)〛 = V) .
+
+(* Esempio banale di divergenza
+unification hint 0 (∀g:group.∀G:list (gcarr g).∀x.
+ V ≟ 〚x,G〛
+ ------------------------------------
+ 〚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.