---

Step * of Lemma id-member-normal-form

∀[x,L:Top].  (rec-case(L) of [] => ff | a::_ => r.if a=2 x then tt else r ~ x ∈b L))
BY
{ (UniformUnivCD Auto THEN SymbComp 0 THEN Auto) }

---

Latex:


\mforall{}[x,L:Top].    (rec-case(L)  of  []  =>  ff  |  a::$_{}$  =>  r.if  a=2  x  then  tt  else  r  \msim{}  \000Cx  \mmember{}\msubb{}  L))


By

(UniformUnivCD  Auto  THEN  SymbComp  0  THEN  Auto)

---

Home Index