Nuprl Lemma : zero-add

[x:ℤ]. (0 x)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] add: m natural_number: $n int: sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T}
Lemmas referenced :  subtype_base_sq int_subtype_base
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation addZero hypothesisEquality hypothesis intEquality isect_memberFormation introduction sqequalAxiom sqequalHypSubstitution dependent_functionElimination thin instantiate lemma_by_obid isectElimination cumulativity independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination

Latex:
\mforall{}[x:\mBbbZ{}].  (0  +  x  \msim{}  x)



Date html generated: 2016_05_13-PM-03_28_53
Last ObjectModification: 2015_12_26-AM-09_48_03

Theory : arithmetic


Home Index