---

Step * 1 1 of Lemma tupletype_cons_lemma


1. L : Top@i
2. T : Top@i
⊢ if null(L) then T else T × rec-case(L) of [] => Unit | h::t => r.if null(t) then h else h × r fi  fi  ~ if null(L)
then T
else T × tuple-type(L)
fi 
BY
{ RW (AddrC [2] (UnfoldC `tuple-type`⋅)) 0⋅ }

1
1. L : Top@i
2. T : Top@i
⊢ if null(L) then T else T × rec-case(L) of [] => Unit | h::t => r.if null(t) then h else h × r fi  fi  ~ if null(L)
then T
else T × rec-case(L) of
         [] => Unit
         T::Ts =>
          r.if null(Ts) then T else T × r fi 
fi 

---

Latex:

---

Latex:

1.  L  :  Top@i
2.  T  :  Top@i
\mvdash{}  if  null(L)
then  T
else  T  \mtimes{}  rec-case(L)  of
                  []  =>  Unit
                  h::t  =>
                    r.if  null(t)  then  h  else  h  \mtimes{}  r  fi 
fi    \msim{}  if  null(L)  then  T  else  T  \mtimes{}  tuple-type(L)  fi 


By

---

Latex:
RW  (AddrC  [2]  (UnfoldC  `tuple-type`\mcdot{}))  0\mcdot{}

---

Home Index