---

Step * 1 of Lemma sq_stable__ex-approx


1. [e] : Atom2
2. [t] : Base
3. [t'] : Base
4. ↓ex-approx(e;t;t')
⊢ ex-approx(e;t;t')
BY
{ (RepeatFor 2 ((At ⌜Type⌝ (D 0)⋅ THENA Auto)) THEN D -3 THEN (Unhide THENW Auto)) }

1
1. e : Atom2
2. t : Base
3. t' : Base
4. ex-approx(e;t;t')
5. f : Base
6. e#f:Base
⊢ f t?e:v.⊥ ≤ f t'?e:v.⊥

---

Latex:

---

Latex:

1.  [e]  :  Atom2
2.  [t]  :  Base
3.  [t']  :  Base
4.  \mdownarrow{}ex-approx(e;t;t')
\mvdash{}  ex-approx(e;t;t')


By

---

Latex:
(RepeatFor  2  ((At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))  THEN  D  -3  THEN  (Unhide  THENW  Auto))

---

Home Index