---

Step * 1 of Lemma tupletype_cons_lemma


1. L : Top@i
2. T : Top@i
⊢ tuple-type([T / L]) ~ if null(L) then T else T × tuple-type(L) fi 
BY
{ RW (AddrC [1] (UnfoldC `tuple-type` ANDTHENC ReduceC)) 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 × tuple-type(L)
fi 

---

Latex:

---

Latex:

1.  L  :  Top@i
2.  T  :  Top@i
\mvdash{}  tuple-type([T  /  L])  \msim{}  if  null(L)  then  T  else  T  \mtimes{}  tuple-type(L)  fi 


By

---

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

---

Home Index