---

Step * 2 of Lemma oal_mon_wf


1. a : LOSet@i'
2. b : AbDMon@i'
⊢ Assoc(|oal(a;b)|;λx,y. (x ++ y))
BY
{ Unfold `assoc` 0  
THEN AbReduceIf (\e t.not is_term `set_car` t) 0 
THEN ((RepD THENM BLemma `oal_merge_assoc`) THENA Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  LOSet@i'
2.  b  :  AbDMon@i'
\mvdash{}  Assoc(|oal(a;b)|;\mlambda{}x,y.  (x  ++  y))


By

---

Latex:
Unfold  `assoc`  0   
THEN  AbReduceIf  (\mbackslash{}e  t.not  is\_term  `set\_car`  t)  0 
THEN  ((RepD  THENM  BLemma  `oal\_merge\_assoc`)  THENA  Auto)\mcdot{}

---

Home Index