---

Step * of Lemma sq_stable_sqle

∀[a,b:Base].  SqStable(a ≤ b)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN UseWitness ⌜Ax⌝⋅
   THEN D -1
   THEN Unfold `member` 0
   THEN Refine `axiomSqleEquality` []
   THEN Hypothesis) }

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    SqStable(a  \mleq{}  b)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  D  -1
  THEN  Unfold  `member`  0
  THEN  Refine  `axiomSqleEquality`  []
  THEN  Hypothesis)

---

Home Index