Nuprl Lemma : decidable__equal_int
∀x,y:ℤ. Dec(x = y ∈ ℤ)
Proof
Definitions occuring in Statement :
decidable: Dec(P),
all: ∀x:A. B[x],
int: ℤ,
equal: s = t ∈ T
Lemmas referenced :
decidable__int_equal
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}x,y:\mBbbZ{}. Dec(x = y)
Date html generated:
2016_05_14-AM-06_44_02
Last ObjectModification:
2015_12_26-PM-00_27_47
Theory : list_0
Home
Index