### Nuprl Lemma : repn_wf

`∀[T:Type]. ∀[x:T]. ∀[n:ℕ].  (repn(n;x) ∈ {z:T| z = x ∈ T}  List)`

Proof

Definitions occuring in Statement :  repn: `repn(n;x)` list: `T List` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` repn: `repn(n;x)` prop: `ℙ` nat: `ℕ`
Lemmas referenced :  primrec_wf list_wf equal_wf nil_wf cons_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin setEquality cumulativity hypothesisEquality because_Cache hypothesis lambdaEquality dependent_set_memberEquality natural_numberEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[n:\mBbbN{}].    (repn(n;x)  \mmember{}  \{z:T|  z  =  x\}    List)

Date html generated: 2017_04_17-AM-07_49_41
Last ObjectModification: 2017_02_27-PM-04_23_28

Theory : list_1

Home Index