---

Step * 6 2 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
⊢ Ident(|omral(g;r)|;λx,y. (x ** y);11)
BY
{ ((AGenRepD ["basic"] 
THENM Force `5` (Reduce 0) 
THENM Backchain  
  ``omral_times_ident_l omral_times_ident_r``) THENA Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
\mvdash{}  Ident(|omral(g;r)|;\mlambda{}x,y.  (x  **  y);11)


By

---

Latex:
((AGenRepD  ["basic"] 
THENM  Force  `5`  (Reduce  0) 
THENM  Backchain   
    ``omral\_times\_ident\_l  omral\_times\_ident\_r``)  THENA  Auto)

---

Home Index