---

Step * of Lemma csm-pi_comp

∀[X,Y,tau,A,cA,cB:Top].  ((pi_comp(X;A;cA;cB))tau ~ pi_comp(Y;(A)tau;(cA)tau;(cB)tau+))
BY
{ Intros }

1
1. [X] : Top
2. [Y] : Top
3. [tau] : Top
4. [A] : Top
5. [cA] : Top
6. [cB] : Top
⊢ (pi_comp(X;A;cA;cB))tau ~ pi_comp(Y;(A)tau;(cA)tau;(cB)tau+)

---

Latex:

---

Latex:
\mforall{}[X,Y,tau,A,cA,cB:Top].    ((pi\_comp(X;A;cA;cB))tau  \msim{}  pi\_comp(Y;(A)tau;(cA)tau;(cB)tau+))


By

---

Latex:
Intros

---

Home Index