---

Step * of Lemma csm-case-type

∀[phi,A,B,s:Top].  (((if phi then A else B))s ~ (if (phi)s then (A)s else (B)s))
BY
{ (Auto THEN RepUR ``case-type case-cube`` 0 THEN CsmUnfolding THEN RepeatFor 4 ((EqCD THEN Try (Trivial)))) }

1
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. a : Base
⊢ A(s I a) ~ let A,F = A 
             in <λI,a. (A I (s I a)), λI,J,f,a,u. (F I J f (s I a) u)>(a)

2
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. a : Base
⊢ B(s I a) ~ let A,F = B 
             in <λI,a. (A I (s I a)), λI,J,f,a,u. (F I J f (s I a) u)>(a)

3
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. J : Base
7. f : Base
⊢ λa,u. if (phi I (s I a)==1) then (u s I a f) else (u s I a f) fi  ~ λrho,c. if (phi I (s I rho)==1)
                                                                         then (c rho f)
                                                                         else (c rho f)
                                                                         fi 

---

Latex:

---

Latex:
\mforall{}[phi,A,B,s:Top].    (((if  phi  then  A  else  B))s  \msim{}  (if  (phi)s  then  (A)s  else  (B)s))


By

---

Latex:
(Auto
  THEN  RepUR  ``case-type  case-cube``  0
  THEN  CsmUnfolding
  THEN  RepeatFor  4  ((EqCD  THEN  Try  (Trivial))))

---

Home Index