### Nuprl Lemma : mklist_wf

`∀[T:Type]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T].  (mklist(n;f) ∈ T List)`

Proof

Definitions occuring in Statement :  mklist: `mklist(n;f)` list: `T List` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` mklist: `mklist(n;f)` nat: `ℕ`
Lemmas referenced :  primrec_wf list_wf nil_wf append_wf cons_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality applyEquality natural_numberEquality setElimination rename because_Cache axiomEquality equalityTransitivity equalitySymmetry Error :functionIsType,  Error :universeIsType,  isect_memberEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  T].    (mklist(n;f)  \mmember{}  T  List)

Date html generated: 2019_06_20-PM-01_31_04
Last ObjectModification: 2018_09_26-PM-05_51_05

Theory : list_1

Home Index