---

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

∀[T:Top]. (((T)p)SigmaUnElim ~ ((T)p)p)
BY
{ ((D 0 THENA Auto) THEN RepUR ``sigma-unelim-pscm`` 0 THEN PscmUnfolding) }

1
1. T : Top
⊢ let A,F = let A,F = T 
            in <λI,a. (A I (fst(a))), λI,J,f,a,u. (F I J f (fst(a)) u)> 
  in <λI,a. (A I let au,v = a in let a,u = au in <a, u, v>)
     , λI,J,f,a,u. (F I J f let au,v = a in let a,u = au in <a, u, v> u)
     > ~ let A,F = let A,F = T 
                   in <λI,a. (A I (fst(a))), λI,J,f,a,u. (F I J f (fst(a)) u)> 
         in <λI,a. (A I (fst(a))), λI,J,f,a,u. (F I J f (fst(a)) u)>

---

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)

---

Home Index