### Nuprl Lemma : comb_for_listify_wf

λT,m,n,f,z. listify(f;m;n) ∈ T:Type ⟶ m:ℤ ⟶ n:ℤ ⟶ f:({m..n-} ⟶ T) ⟶ (↓True) ⟶ (T List)

Proof

Definitions occuring in Statement :  listify: listify(f;m;n) list: List int_seg: {i..j-} squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x] int: universe: Type
Definitions unfolded in proof :  member: t ∈ T squash: T uall: [x:A]. B[x] prop:
Lemmas referenced :  listify_wf squash_wf true_wf int_seg_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaEquality_alt,  sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry Error :universeIsType,  Error :functionIsType,  Error :inhabitedIsType,  universeEquality

Latex:
\mlambda{}T,m,n,f,z.  listify(f;m;n)  \mmember{}  T:Type  {}\mrightarrow{}  m:\mBbbZ{}  {}\mrightarrow{}  n:\mBbbZ{}  {}\mrightarrow{}  f:(\{m..n\msupminus{}\}  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  (T  List)

Date html generated: 2019_06_20-PM-00_38_28
Last ObjectModification: 2018_10_02-PM-05_40_42

Theory : list_0

Home Index