---

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


1. T : Top
2. A : Base
3. F : Base
4. I : Base
5. J : Base
6. f : Base
7. a : Base
8. u : Base
⊢ F I J f (fst(let au,v = a in let a,u = au in <a, u, v>)) ~ F I J f (fst(fst(a)))
BY
{ (EqCD THEN Try (Trivial)) }

1
1. T : Top
2. A : Base
3. F : Base
4. I : Base
5. J : Base
6. f : Base
7. a : Base
8. u : Base
⊢ fst(let au,v = a 
      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