---

Step * of Lemma sq_stable__sqequal_n

∀[x,y:Base]. ∀[n:ℕ].  SqStable(x ~n y)
BY
{ (Auto THEN D 0 THEN Auto THEN UseWitness ⌜Ax⌝⋅ THEN D -1) }

1
1. x : Base
2. y : Base
3. n : ℕ
4. x ~n y
⊢ Ax ∈ x ~n y

---

Latex:

---

Latex:
\mforall{}[x,y:Base].  \mforall{}[n:\mBbbN{}].    SqStable(x  \msim{}n  y)


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  D  -1)

---

Home Index