---

Step * of Lemma tupletype_cons_lemma

∀L,T:Top.  (tuple-type([T / L]) ~ if null(L) then T else T × tuple-type(L) fi )
BY
{ (UnivCD THENA Auto) }

1
1. L : Top@i
2. T : Top@i
⊢ tuple-type([T / L]) ~ if null(L) then T else T × tuple-type(L) fi 

---

Latex:

---

Latex:
\mforall{}L,T:Top.    (tuple-type([T  /  L])  \msim{}  if  null(L)  then  T  else  T  \mtimes{}  tuple-type(L)  fi  )


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index