---

Step * of Lemma equiv-comp_wf

No Annotations
∀[H:j⊢]. ∀[A,E:{H ⊢ _}]. ∀[cA:H ⊢ CompOp(A)]. ∀[cE:H ⊢ CompOp(E)].  (equiv-comp(H;A;E;cA;cE) ∈ H ⊢ CompOp(Equiv(A;E)))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[A,E:\{H  \mvdash{}  \_\}].  \mforall{}[cA:H  \mvdash{}  CompOp(A)].  \mforall{}[cE:H  \mvdash{}  CompOp(E)].
    (equiv-comp(H;A;E;cA;cE)  \mmember{}  H  \mvdash{}  CompOp(Equiv(A;E)))


By

---

Latex:
ProveWfLemma

---

Home Index