---

Step * 1 of Lemma permr_nil_is_nil


1. T : Type
⊢ ([] ≡(T) []) ⇒ ([] = [] ∈ (T List))
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  ([]  \mequiv{}(T)  [])  {}\mRightarrow{}  ([]  =  [])


By

---

Latex:
Auto

---

Home Index