---

Step * 1 of Lemma assert_of_eq_list


1. s : DSet
2. as : |s| List
⊢ ∀bs:|s| List. (↑(as =b bs) ⇐⇒ as = bs ∈ (|s| List))
BY
{ ((ListInd 2 THEN RecCaseSplit `eq_list`) THEN (D 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN Auto) }

1
1. s : DSet
2. u : |s|
3. v : |s| List
4. ∀bs:|s| List. (↑(v =b bs) ⇐⇒ v = bs ∈ (|s| List))
5. u1 : |s|
6. v1 : |s| List
7. ↑((u (=b) u1) ∧b (v =b v1))
⊢ [u / v] = [u1 / v1] ∈ (|s| List)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  |s|  List
\mvdash{}  \mforall{}bs:|s|  List.  (\muparrow{}(as  =\msubb{}  bs)  \mLeftarrow{}{}\mRightarrow{}  as  =  bs)


By

---

Latex:
((ListInd  2  THEN  RecCaseSplit  `eq\_list`)  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index