---

Step * 1 of Lemma qoset_properties


1. s : DSet
2. [%1] : UniformPreorder(|s|;a,b.a ≤ b)
⊢ SqStable(UniformPreorder(|s|;a,b.a ≤ b))
BY
{ ((D 0 THEN Auto) THEN D -1 THEN UnhideUsingWitness THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  [\%1]  :  UniformPreorder(|s|;a,b.a  \mleq{}  b)
\mvdash{}  SqStable(UniformPreorder(|s|;a,b.a  \mleq{}  b))


By

---

Latex:
((D  0  THEN  Auto)  THEN  D  -1  THEN  UnhideUsingWitness  THEN  Auto)

---

Home Index