---

Step * of Lemma rev-type-line-comp_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)].  ((cA)- ∈ Gamma.𝕀 ⊢ CompOp((A)-))
BY
{ (Auto THEN Unfolds ``rev-type-line rev-type-line-comp`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  CompOp(A)].    ((cA)-  \mmember{}  Gamma.\mBbbI{}  \mvdash{}  CompOp((A)-))


By

---

Latex:
(Auto  THEN  Unfolds  ``rev-type-line  rev-type-line-comp``  0  THEN  Auto)

---

Home Index