Step * 1 3 of Lemma qadd_grp_wf


Inverse(ℚx,y. (x y);0;λx.-(x))
BY
(RepUR ``inverse`` THEN Auto) }


Latex:


Latex:

Inverse(\mBbbQ{};\mlambda{}x,y.  (x  +  y);0;\mlambda{}x.-(x))


By


Latex:
(RepUR  ``inverse``  0  THEN  Auto)




Home Index