Nuprl Lemma : nat_plus_inc
ℕ+ ⊆r ℕ
Proof
Definitions occuring in Statement :
nat_plus: ℕ+,
nat: ℕ,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T
Lemmas referenced :
nat_plus_subtype_nat,
nat_plus_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
cut,
hypothesisEquality,
applyEquality,
thin,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalRule
Latex:
\mBbbN{}\msupplus{} \msubseteq{}r \mBbbN{}
Date html generated:
2019_06_20-AM-11_33_33
Last ObjectModification:
2018_09_17-PM-05_36_19
Theory : int_1
Home
Index