---

Step * of Lemma list-cases2

∀[T:Type]. ∀x:T List. ((x ~ []) ∨ (x ~ [hd(x) / tl(x)]))
BY
{ (Auto THEN D -1 THEN Auto THEN Reduce 0 THEN OrRight THEN Try (Complete (Auto))) }

1
.....wf..... 
1. T : Type
2. u : T
3. v : T List
⊢ istype([u / v] ~ [])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T  List.  ((x  \msim{}  [])  \mvee{}  (x  \msim{}  [hd(x)  /  tl(x)]))


By

---

Latex:
(Auto  THEN  D  -1  THEN  Auto  THEN  Reduce  0  THEN  OrRight  THEN  Try  (Complete  (Auto)))

---

Home Index