---

Step * of Lemma null_functionality_wrt_permr

∀T:Type. ∀as,bs:T List.  ((as ≡(T) bs) ⇒ null(as) = null(bs))
BY
{ (RepeatMFor 3 (D 0) THENA Auto) }

1
1. T : Type
2. as : T List
3. bs : T List
⊢ (as ≡(T) bs) ⇒ null(as) = null(bs)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as,bs:T  List.    ((as  \mequiv{}(T)  bs)  {}\mRightarrow{}  null(as)  =  null(bs))


By

---

Latex:
(RepeatMFor  3  (D  0)  THENA  Auto)

---

Home Index