Nuprl Lemma : tupletype_cons_lemma

L,T:Top.  (tuple-type([T L]) if null(L) then else T × tuple-type(L) fi )


Proof




Definitions occuring in Statement :  tuple-type: tuple-type(L) null: null(as) cons: [a b] ifthenelse: if then else fi  top: Top all: x:A. B[x] product: x:A × B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T tuple-type: tuple-type(L) so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3]
Lemmas referenced :  top_wf list_ind_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

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



Date html generated: 2016_05_14-PM-03_57_26
Last ObjectModification: 2015_12_26-PM-07_22_14

Theory : tuples


Home Index