Nuprl Lemma : nat-deq-aux

[a,b:ℕ].  uiff(a b ∈ ℕ;↑(a =z b))


Proof




Definitions occuring in Statement :  nat: assert: b eq_int: (i =z j) uiff: uiff(P;Q) uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a nat: squash: T member: t ∈ T le: A ≤ B prop: uall: [x:A]. B[x] rev_implies:  Q implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  equal_wf nat_wf le_wf iff_weakening_uiff assert_wf eq_int_wf assert_of_eq_int assert_witness uiff_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation sqequalHypSubstitution applyLambdaEquality setElimination thin rename hypothesis sqequalRule imageMemberEquality hypothesisEquality baseClosed introduction productElimination extract_by_obid isectElimination dependent_set_memberEquality natural_numberEquality intEquality addLevel independent_isectElimination because_Cache independent_functionElimination cumulativity independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[a,b:\mBbbN{}].    uiff(a  =  b;\muparrow{}(a  =\msubz{}  b))



Date html generated: 2019_06_20-PM-00_31_54
Last ObjectModification: 2018_08_24-PM-10_58_43

Theory : equality!deciders


Home Index