---

Step * of Lemma pres-a0_wf

No Annotations
∀[G:j⊢]. ∀[A,T:{G.𝕀 ⊢ _}]. ∀[f:{G.𝕀 ⊢ _:(T ⟶ A)}]. ∀[t0:{G ⊢ _:(T)[0(𝕀)]}].  (pres-a0(G;f;t0) ∈ {G ⊢ _:(A)[0(𝕀)]})
BY
{ (Intros
   THEN (Assert (f)[0(𝕀)] ∈ {G ⊢ _:((T)[0(𝕀)] ⟶ (A)[0(𝕀)])} BY
               ((Assert (f)[0(𝕀)] ∈ {G ⊢ _:((T ⟶ A))[0(𝕀)]} BY Auto) THEN InferEqualType THEN Auto))
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,T:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[f:\{G.\mBbbI{}  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[t0:\{G  \mvdash{}  \_:(T)[0(\mBbbI{})]\}].
    (pres-a0(G;f;t0)  \mmember{}  \{G  \mvdash{}  \_:(A)[0(\mBbbI{})]\})


By

---

Latex:
(Intros
  THEN  (Assert  (f)[0(\mBbbI{})]  \mmember{}  \{G  \mvdash{}  \_:((T)[0(\mBbbI{})]  {}\mrightarrow{}  (A)[0(\mBbbI{})])\}  BY
                          ((Assert  (f)[0(\mBbbI{})]  \mmember{}  \{G  \mvdash{}  \_:((T  {}\mrightarrow{}  A))[0(\mBbbI{})]\}  BY  Auto)  THEN  InferEqualType  THEN  Auto))
  THEN  ProveWfLemma)

---

Home Index