---

Step * of Lemma sq_stable__ex-approx

∀[e:Atom2]. ∀[t,t':Base].  SqStable(ex-approx(e;t;t'))
BY
{ (Intros THEN (D 0 THENW Auto)) }

1
1. [e] : Atom2
2. [t] : Base
3. [t'] : Base
4. ↓ex-approx(e;t;t')
⊢ ex-approx(e;t;t')

---

Latex:

---

Latex:
\mforall{}[e:Atom2].  \mforall{}[t,t':Base].    SqStable(ex-approx(e;t;t'))


By

---

Latex:
(Intros  THEN  (D  0  THENW  Auto))

---

Home Index