---

Step * 3 of Lemma csm-case-type


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 
BY
{ RepeatFor 3 ((EqCD THEN Try (Trivial))) }

1
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. J : Base
7. f : Base
8. a : Base
9. u : Base
⊢ (u s I a f) ~ (u a f)

2
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. J : Base
7. f : Base
8. a : Base
9. u : Base
⊢ (u s I a f) ~ (u a f)

---

Latex:

---

Latex:

1.  phi  :  Top
2.  A  :  Top
3.  B  :  Top
4.  s  :  Top
5.  I  :  Base
6.  J  :  Base
7.  f  :  Base
\mvdash{}  \mlambda{}a,u.  if  (phi  I  (s  I  a)==1)  then  (u  s  I  a  f)  else  (u  s  I  a  f)  fi    \msim{}  \mlambda{}rho,c.  if  (phi  I  (s  I  rho)==1\000C)
                                                                                                                                                  then  (c  rho  f)
                                                                                                                                                  else  (c  rho  f)
                                                                                                                                                  fi 


By

---

Latex:
RepeatFor  3  ((EqCD  THEN  Try  (Trivial)))

---

Home Index