---

Step * 1 of Lemma csm-equiv_comp-sq


1. H : Top
2. K : Top
3. tau : Top
4. A : Top
5. E : Top
6. cA : Top
7. cE : Top
8. ∀[X,cA,cB,A@0,tau@0:Top].  ((sigma_comp(cA;cB))tau@0 ~ sigma_comp((cA)tau@0;(cB)tau@0+))
⊢ (pi_comp(H;A;cA;(cE)p))tau ~ pi_comp(K;(A)tau;(cA)tau;((cE)tau)p)
BY
{ ((InstLemma `csm-pi_comp` [⌜H⌝;⌜K⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)
   THEN RW  (SubC (SymbCompC [] 100)) 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  H  :  Top
2.  K  :  Top
3.  tau  :  Top
4.  A  :  Top
5.  E  :  Top
6.  cA  :  Top
7.  cE  :  Top
8.  \mforall{}[X,cA,cB,A@0,tau@0:Top].    ((sigma\_comp(cA;cB))tau@0  \msim{}  sigma\_comp((cA)tau@0;(cB)tau@0+))
\mvdash{}  (pi\_comp(H;A;cA;(cE)p))tau  \msim{}  pi\_comp(K;(A)tau;(cA)tau;((cE)tau)p)


By

---

Latex:
((InstLemma  `csm-pi\_comp`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  RW    (SubC  (SymbCompC  []  100))  0
  THEN  Auto)

---

Home Index