---

Step * of Lemma sd_ordered_wf

∀s:DSet. ∀as:|s| List.  (sd_ordered(as) ∈ 𝔹)
BY
{ ((UnivCD) THENA Auto) 
THEN OnVar `as' ListInd }

1
1. s : DSet
⊢ sd_ordered([]) ∈ 𝔹

2
1. s : DSet
2. u : |s|
3. v : |s| List
4. sd_ordered(v) ∈ 𝔹
⊢ sd_ordered([u / v]) ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as:|s|  List.    (sd\_ordered(as)  \mmember{}  \mBbbB{})


By

---

Latex:
((UnivCD)  THENA  Auto) 
THEN  OnVar  `as'  ListInd

---

Home Index