---

Step * of Lemma void-list-equality2

∀[x,y:Void List]. ∀[T:Type].  (x = y ∈ (T List))
BY
{ (Auto THEN Subst ⌜x ~ y⌝ 0⋅) }

1
.....equality..... 
1. x : Void List
2. y : Void List
3. T : Type
⊢ x ~ y

2
1. x : Void List
2. y : Void List
3. T : Type
⊢ y = y ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[x,y:Void  List].  \mforall{}[T:Type].    (x  =  y)


By

---

Latex:
(Auto  THEN  Subst  \mkleeneopen{}x  \msim{}  y\mkleeneclose{}  0\mcdot{})

---

Home Index