---

Step * of Lemma l-last-cons

∀[u,v:Top].  (l-last([u / v]) ~ if null(v) then u else l-last(v) fi )
BY
{ ((UnivCD THENA Auto) THEN RepUR ``l-last l-last-default null`` 0 THEN RecUnfold `list_ind` 0⋅ THEN LiftRed ) }

1
1. u : Top
2. v : Top
⊢ eval v = v in
  if v is a pair then let h,t = v 
                      in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then u otherwise ⊥ 
~ if if v is a pair then ff otherwise if v = Ax then tt otherwise ⊥
then u
else eval v = v in
     if v is a pair then let h,t = v 
                         in rec-case(t) of [] => λx.x | h::t => r.λx.(r h) h otherwise if v = Ax then ⊥ otherwise ⊥
fi 

---

Latex:

---

Latex:
\mforall{}[u,v:Top].    (l-last([u  /  v])  \msim{}  if  null(v)  then  u  else  l-last(v)  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``l-last  l-last-default  null``  0
  THEN  RecUnfold  `list\_ind`  0\mcdot{}
  THEN  LiftRed  )

---

Home Index