---

Step * of Lemma equiv-comp-exists

No Annotations
∀H:j⊢. ∀A,E:{H ⊢ _}.  (H ⊢ CompOp(A) ⇒ H ⊢ CompOp(E) ⇒ H ⊢ CompOp(Equiv(A;E)))
BY
{ (Auto THEN RenameVar `cA' (-2) THEN RenameVar `cE' (-1) THEN UseWitness ⌜equiv-comp(H;A;E;cA;cE)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}H:j\mvdash{}.  \mforall{}A,E:\{H  \mvdash{}  \_\}.    (H  \mvdash{}  CompOp(A)  {}\mRightarrow{}  H  \mvdash{}  CompOp(E)  {}\mRightarrow{}  H  \mvdash{}  CompOp(Equiv(A;E)))


By

---

Latex:
(Auto
  THEN  RenameVar  `cA'  (-2)
  THEN  RenameVar  `cE'  (-1)
  THEN  UseWitness  \mkleeneopen{}equiv-comp(H;A;E;cA;cE)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index