〚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.