---

Step * of Lemma csm-universe-comp-fun

No Annotations
∀[s,A,G,H:Top].  ((CompFun(A))s ~ CompFun((A)s))
BY
{ (Auto
   THEN RepUR ``universe-comp-fun`` 0
   THEN (RWO "csm-universe-comp-op<" 0 THENA Auto)
   THEN (GenConcl ⌜compOp(A) = X ∈ Top⌝⋅ THENA Auto)) }

1
1. s : Top
2. A : Top
3. G : Top
4. H : Top
5. X : Top
6. compOp(A) = X ∈ Top
⊢ (cop-to-cfun(X))s ~ cop-to-cfun((X)s)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[s,A,G,H:Top].    ((CompFun(A))s  \msim{}  CompFun((A)s))


By

---

Latex:
(Auto
  THEN  RepUR  ``universe-comp-fun``  0
  THEN  (RWO  "csm-universe-comp-op<"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}compOp(A)  =  X\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index