Step * 3 of Lemma csm-case-type


1. phi Top
2. Top
3. Top
4. Top
5. Base
6. Base
7. Base
⊢ λa,u. if (phi (s a)==1) then (u f) else (u f) fi  ~ λrho,c. if (phi (s rho)==1)
                                                                         then (c rho f)
                                                                         else (c rho f)
                                                                         fi 
BY
RepeatFor ((EqCD THEN Try (Trivial))) }

1
1. phi Top
2. Top
3. Top
4. Top
5. Base
6. Base
7. Base
8. Base
9. Base
⊢ (u f) (u f)

2
1. phi Top
2. Top
3. Top
4. Top
5. Base
6. Base
7. Base
8. Base
9. Base
⊢ (u f) (u 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