---

Step * of Lemma universe-comp-fun_wf

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}].  (CompFun(t) ∈ X +⊢ Compositon(decode(t)))
BY
{ ( Intros⋅ THEN Unhide THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:c\mBbbU{}\}].    (CompFun(t)  \mmember{}  X  +\mvdash{}  Compositon(decode(t)))


By

---

Latex:
(  Intros\mcdot{}  THEN  Unhide  THEN  ProveWfLemma)

---

Home Index