Nuprl Lemma : assert_of_eq_int_rw
∀[x,y:ℤ]. {uiff(↑(x =z y);x = y ∈ ℤ)}
Proof
Definitions occuring in Statement :
assert: ↑b,
eq_int: (i =z j),
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
guard: {T},
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
assert_of_eq_int
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}[x,y:\mBbbZ{}]. \{uiff(\muparrow{}(x =\msubz{} y);x = y)\}
Date html generated:
2016_05_13-PM-03_56_56
Last ObjectModification:
2015_12_26-AM-10_51_57
Theory : bool_1
Home
Index