---

Step * 1 of Lemma null_functionality_wrt_permr


1. T : Type
2. as : T List
3. bs : T List
⊢ (as ≡(T) bs) ⇒ null(as) = null(bs)
BY
{ (OnMHyps [3; 2] (\i. (D i)) THEN AbReduce 0 THEN Auto) }

1
1. T : Type
2. u : T
3. v : T List
4. [u / v] ≡(T) []
⊢ ff = tt

2
1. T : Type
2. u : T
3. v : T List
4. [] ≡(T) [u / v]
⊢ tt = ff

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
\mvdash{}  (as  \mequiv{}(T)  bs)  {}\mRightarrow{}  null(as)  =  null(bs)


By

---

Latex:
(OnMHyps  [3;  2]  (\mbackslash{}i.  (D  i))  THEN  AbReduce  0  THEN  Auto)

---

Home Index