---

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


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)>
BY
{ (RW (SubC (SymbolicComputeStepC)) 0 THEN RepeatFor 2 (EqCD) THEN Computation THEN EqCD THEN Try (Trivial)) }

1
1. T : Top
2. A : Base
3. F : Base
4. I : Base
5. a : Base
⊢ fst(let au,v = a 
      in let a,u = au 
         in <a, u, v>) ~ fst(fst(a))

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

---

Latex:

---

Latex:

1.  T  :  Top
\mvdash{}  let  A,F  =  let  A,F  =  T 
                        in  <\mlambda{}I,a.  (A  I  (fst(a))),  \mlambda{}I,J,f,a,u.  (F  I  J  f  (fst(a))  u)> 
    in  <\mlambda{}I,a.  (A  I  let  au,v  =  a  in  let  a,u  =  au  in  <a,  u,  v>)
          ,  \mlambda{}I,J,f,a,u.  (F  I  J  f  let  au,v  =  a  in  let  a,u  =  au  in  <a,  u,  v>  u)
          >  \msim{}  let  A,F  =  let  A,F  =  T 
                                      in  <\mlambda{}I,a.  (A  I  (fst(a))),  \mlambda{}I,J,f,a,u.  (F  I  J  f  (fst(a))  u)> 
                  in  <\mlambda{}I,a.  (A  I  (fst(a))),  \mlambda{}I,J,f,a,u.  (F  I  J  f  (fst(a))  u)>


By

---

Latex:
(RW  (SubC  (SymbolicComputeStepC))  0
  THEN  RepeatFor  2  (EqCD)
  THEN  Computation
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index