---

Step * 1 of Lemma void-list-equality2

.....equality..... 
1. x : Void List
2. y : Void List
3. T : Type
⊢ x ~ y
BY
{ (BLemma `void-list-equality` THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  Void  List
2.  y  :  Void  List
3.  T  :  Type
\mvdash{}  x  \msim{}  y


By

---

Latex:
(BLemma  `void-list-equality`  THEN  Auto)

---

Home Index