---

Step * 3 of Lemma oal_mon_wf


1. a : LOSet@i'
2. b : AbDMon@i'
⊢ Ident(|oal(a;b)|;λx,y. (x ++ y);00)
BY
{ Unfold `ident` 0  
THEN AbReduceIf (\e t.not is_term `set_car` t) 0 
THEN ((GenRepD) THENA Auto) 
 }

1
1. a : LOSet@i'
2. b : AbDMon@i'
3. x : |oal(a;b)|
⊢ (x ++ 00) = x ∈ |oal(a;b)|

2
1. a : LOSet@i'
2. b : AbDMon@i'
3. x : |oal(a;b)|
⊢ (00 ++ x) = x ∈ |oal(a;b)|

---

Latex:

---

Latex:

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


By

---

Latex:
Unfold  `ident`  0   
THEN  AbReduceIf  (\mbackslash{}e  t.not  is\_term  `set\_car`  t)  0 
THEN  ((GenRepD)  THENA  Auto) 

---

Home Index