---

Step * of Lemma sq_stable__sqle

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

---

Latex:

---

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


By

---

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

---

Home Index