---

Step * of Lemma ex-approx-context

No Annotations
∀[e:Atom2]. ∀[a,b,g:Base].  (ex-approx(e;g a;g b)) supposing (ex-approx(e;a;b) and e#g:Base)
BY
{ (RepeatFor 4 (Intro) THEN RepeatFor 2 (At ⌜Type⌝ Intro⋅) THEN (Unhide THENA Auto)) }

1
1. e : Atom2
2. a : Base
3. b : Base
4. g : Base
5. e#g:Base
6. ex-approx(e;a;b)
⊢ ex-approx(e;g a;g b)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[e:Atom2].  \mforall{}[a,b,g:Base].    (ex-approx(e;g  a;g  b))  supposing  (ex-approx(e;a;b)  and  e\#g:Base)


By

---

Latex:
(RepeatFor  4  (Intro)  THEN  RepeatFor  2  (At  \mkleeneopen{}Type\mkleeneclose{}  Intro\mcdot{})  THEN  (Unhide  THENA  Auto))

---

Home Index