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


1. Top
2. Base
3. Base
4. Base
5. Base
⊢ fst(let au,v 
      in let a,u au 
         in <a, u, v>fst(fst(a))
BY
(Unfold `pi1` THEN RepeatFor ((RW (SubC (SymbolicComputeStepC)) THEN EqCD THEN Try (Trivial)))) }


Latex:


Latex:

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


By


Latex:
(Unfold  `pi1`  0
  THEN  RepeatFor  2  ((RW  (SubC  (SymbolicComputeStepC))  0  THEN  EqCD  THEN  Try  (Trivial)))
  )




Home Index