Nuprl Lemma : nat_plus_wf

+ ∈ Type


Proof




Definitions occuring in Statement :  nat_plus: + member: t ∈ T universe: Type
Definitions unfolded in proof :  nat_plus: + member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] prop: so_apply: x[s]
Lemmas referenced :  set_wf less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache sqequalRule lambdaEquality natural_numberEquality hypothesisEquality hypothesis intEquality

Latex:
\mBbbN{}\msupplus{}  \mmember{}  Type



Date html generated: 2016_05_13-PM-03_32_10
Last ObjectModification: 2015_12_26-AM-09_45_29

Theory : arithmetic


Home Index