---

Step * of Lemma comp_term-composition-term

∀[Gamma,phi,cA,u,a0:Top].  (comp cop-to-cfun(cA) [phi ⊢→ u] a0 ~ comp cA [phi ⊢→ u] a0)
BY
{ (Intros THEN RepUR ``composition-term comp_term comp-op-to-comp-fun csm-composition`` 0 THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Gamma,phi,cA,u,a0:Top].    (comp  cop-to-cfun(cA)  [phi  \mvdash{}\mrightarrow{}  u]  a0  \msim{}  comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)


By

---

Latex:
(Intros
  THEN  RepUR  ``composition-term  comp\_term  comp-op-to-comp-fun  csm-composition``  0
  THEN  CsmUnfolding
  THEN  Auto)

---

Home Index