---

Step * of Lemma list-cases

∀[T:Type]. ∀x:T List. ((x ~ []) ∨ (x ∈ T × (T List)))
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. [T] : Type
2. x : T List
⊢ (x ~ []) ∨ (x ∈ T × (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T  List.  ((x  \msim{}  [])  \mvee{}  (x  \mmember{}  T  \mtimes{}  (T  List)))


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index