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