Step * 1 2 of Lemma ps-sigma-unelim-p-type


1. Top
2. Base
3. Base
4. Base
5. Base
6. Base
7. Base
8. Base
⊢ (fst(let au,v in let a,u au in <a, u, v>)) (fst(fst(a)))
BY
(EqCD THEN Try (Trivial)) }

1
1. Top
2. Base
3. Base
4. Base
5. Base
6. Base
7. Base
8. Base
⊢ fst(let au,v 
      in let a,u au 
         in <a, u, v>fst(fst(a))


Latex:


Latex:

1.  T  :  Top
2.  A  :  Base
3.  F  :  Base
4.  I  :  Base
5.  J  :  Base
6.  f  :  Base
7.  a  :  Base
8.  u  :  Base
\mvdash{}  F  I  J  f  (fst(let  au,v  =  a  in  let  a,u  =  au  in  <a,  u,  v>))  \msim{}  F  I  J  f  (fst(fst(a)))


By


Latex:
(EqCD  THEN  Try  (Trivial))




Home Index