---

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

∀[t:Top]. (((t)p)SigmaUnElim ~ ((t)p)p)
BY
{ ((D 0 THENA Auto) THEN RepUR ``sigma-unelim-pscm`` 0 THEN PscmUnfolding THEN RepeatFor 3 (EqCD) THEN Try (Trivial)) }

1
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))

---

Latex:

---

Latex:
\mforall{}[t:Top].  (((t)p)SigmaUnElim  \msim{}  ((t)p)p)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepUR  ``sigma-unelim-pscm``  0
  THEN  PscmUnfolding
  THEN  RepeatFor  3  (EqCD)
  THEN  Try  (Trivial))

---

Home Index