---

Step * 1 2 of Lemma dM-lift-sq


1. I' : Top
2. J' : Top
3. I : Top
4. J : Top
5. f : Top
6. ac : Base
7. xs : Base
8. p : Base
9. a : Base
10. v : Base
11. a@0 : Base
12. as' : Base
⊢ (λx,y. x ∨ y) a@0 
  (fix((λlist_ind,L. eval v = L in
                     if v is a pair then let a,as' = v 
                                         in (λx,y. x ∨ y) a (list_ind as') otherwise if v = Ax then 0 otherwise ⊥)) 
   as') ~ (λx,y. x ∨ y) a@0 
          (fix((λlist_ind,L. eval v = L in
                             if v is a pair then let a,as' = v 
                                                 in (λx,y. x ∨ y) a (list_ind as') otherwise if v = Ax then 0 otherwise \000C⊥)) 
           as')
BY
{ RepeatFor 4 ((EqCD THEN Try (Trivial))) }

1
1. I' : Top
2. J' : Top
3. I : Top
4. J : Top
5. f : Top
6. ac : Base
7. xs : Base
8. p : Base
9. a : Base
10. v : Base
11. a@0 : Base
12. as' : Base
13. x : Base
14. y : Base
⊢ x ∨ y ~ x ∨ y

2
1. I' : Top
2. J' : Top
3. I : Top
4. J : Top
5. f : Top
6. ac : Base
7. xs : Base
8. p : Base
9. a : Base
10. v : Base
11. a@0 : Base
12. as' : Base
13. list_ind : Base
⊢ λL.eval v = L in
     if v is a pair then let a,as' = v 
                         in (λx,y. x ∨ y) a (list_ind as') otherwise if v = Ax then 0 otherwise ⊥ ~ λL.eval v = L in
                                                                                                   if v is a pair
                                                                                                   then let a,as' = v 
                                                                                                        in (λx,y. x ∨ y)\000C a 
                                                                                                           (list_ind 
                                                                                                            as')
                                                                                                   otherwise if v = Ax
                                                                                                             then 0
                                                                                                             otherwise ⊥

---

Latex:

---

Latex:

1.  I'  :  Top
2.  J'  :  Top
3.  I  :  Top
4.  J  :  Top
5.  f  :  Top
6.  ac  :  Base
7.  xs  :  Base
8.  p  :  Base
9.  a  :  Base
10.  v  :  Base
11.  a@0  :  Base
12.  as'  :  Base
\mvdash{}  (\mlambda{}x,y.  x  \mvee{}  y)  a@0 
    (fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                        if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                in  (\mlambda{}x,y.  x  \mvee{}  y)  a  (list$_{ind}$  as')
                                        otherwise  if  v  =  Ax  then  0  otherwise  \mbot{})) 
      as')  \msim{}  (\mlambda{}x,y.  x  \mvee{}  y)  a@0 
                    (fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                        if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                                in  (\mlambda{}x,y.  x  \mvee{}  y)  a  (list$_{ind}$\000C  as')
                                                        otherwise  if  v  =  Ax  then  0  otherwise  \mbot{})) 
                      as')


By

---

Latex:
RepeatFor  4  ((EqCD  THEN  Try  (Trivial)))

---

Home Index