---

Step * of Lemma es-le-first

∀[es:EO]. ∀[j,e:E].  if first(j) then j else e fi  = e ∈ E supposing e ≤loc j 
BY
{ (Auto THEN SplitOnConclITE THEN Auto) }

1
.....truecase..... 
1. es : EO
2. j : E
3. e : E
4. e ≤loc j 
5. ↑first(j)
⊢ j = e ∈ E

---

Latex:


\mforall{}[es:EO].  \mforall{}[j,e:E].    if  first(j)  then  j  else  e  fi    =  e  supposing  e  \mleq{}loc  j 


By

(Auto  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index