Nuprl Rule : isintReduceTrue
This rule proved as lemma rule_isint_reduce_true_true3 in file rules/rules_isint.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ if z is an integer then a else b ~ a
BY isintReduceTrue ()
H ⊢ z = z ∈ ℤ
Definitions occuring in rule :
sqequal: s ~ t,
isint: isint def,
equal: s = t ∈ T,
int: ℤ,
axiom: Ax
Latex:
H \mvdash{} if z is an integer then a else b \msim{} a
BY isintReduceTrue ()
H \mvdash{} z = z
Date html generated:
2019_06_20-PM-04_12_02
Last ObjectModification:
2016_07_08-PM-03_48_52
Theory : rules
Home
Index