---

Step * 1 1 of Lemma sq_stable__ex-approx


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.⊥
BY
{ (D -3 With ⌜f⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  Atom2
2.  t  :  Base
3.  t'  :  Base
4.  ex-approx(e;t;t')
5.  f  :  Base
6.  e\#f:Base
\mvdash{}  f  t?e:v.\mbot{}  \mleq{}  f  t'?e:v.\mbot{}


By

---

Latex:
(D  -3  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index