---

Step * of Lemma csm-case-type-comp

∀[H,Gamma,tau,phi,psi,A,B,cA,cB:Top].
  ((case-type-comp(Gamma; phi; psi; A; B; cA; cB))tau ~ case-type-comp(H;
                                                                       (phi)tau;
                                                                       (psi)tau;
                                                                       (A)tau;
                                                                       (B)tau;
                                                                       (cA)tau;
                                                                       (cB)tau))
BY
{ (Intros THEN Unfold `case-type-comp` 0 THEN RepUR ``csm-comp-structure`` 0 THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[H,Gamma,tau,phi,psi,A,B,cA,cB:Top].
    ((case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB))tau  \msim{}  case-type-comp(H;
                                                                                                                                              (phi)tau;
                                                                                                                                              (psi)tau;
                                                                                                                                              (A)tau;
                                                                                                                                              (B)tau;
                                                                                                                                              (cA)tau;
                                                                                                                                              (cB)tau))


By

---

Latex:
(Intros
  THEN  Unfold  `case-type-comp`  0
  THEN  RepUR  ``csm-comp-structure``  0
  THEN  CsmUnfolding
  THEN  Auto)

---

Home Index