---

Step * 1 2 of Lemma hgrp_of_ocgrp_wf2


1. g : OGrp
⊢ RelsIso(|g|+;|g|;x,y.↑(x =b y);x,y.↑(x =b y);λx.x)
BY
{ ((ARepD ["basic"] THENM Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OGrp
\mvdash{}  RelsIso(|g|\msupplus{};|g|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);\mlambda{}x.x)


By

---

Latex:
((ARepD  ["basic"]  THENM  Reduce  0)  THEN  Auto)

---

Home Index