---

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


1. t : Top
2. I : Base
3. a : Base
⊢ fst(let au,v = a 
      in let a,u = au 
         in <a, u, v>) ~ fst(fst(a))
BY
{ (Unfold `pi1` 0 THEN RepeatFor 2 ((RW (SubC (SymbolicComputeStepC)) 0 THEN EqCD THEN Try (Trivial)))) }

---

Latex:

---

Latex:

1.  t  :  Top
2.  I  :  Base
3.  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