---

Step * of Lemma univ-trans_wf

No Annotations
∀[G:j⊢]. ∀[T:{G.𝕀 ⊢ _:c𝕌}].  (univ-trans(G;T) ∈ {G ⊢ _:((decode(T))[0(𝕀)] ⟶ (decode(T))[1(𝕀)])})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[T:\{G.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}].    (univ-trans(G;T)  \mmember{}  \{G  \mvdash{}  \_:((decode(T))[0(\mBbbI{})]  {}\mrightarrow{}  (decode(T))[1(\mBbbI{})])\})


By

---

Latex:
ProveWfLemma

---

Home Index