Nuprl Rule : isaxiomCases

This rule proved as lemma rule_isaxiom_cases_true in file rules/rules_axiom_cases.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext !((!\\x.if t = Ax then ea otherwise eb) Ax)

  BY isaxiomCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ Ax) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t = Ax then u otherwise v ~ v)) ⊢ C ext eb

Definitions occuring in rule : sqle: s ≤ t, callbyvalue: callbyvalue, natural_number: $n, member: t ∈ T, axiom: Ax, uall: ∀[x:A]. B[x], base: Base, sqequal: s ~ t, isaxiom: if z = Ax then a otherwise b

Latex:
H \mvdash{} C ext !((!\mbackslash{}\mbackslash{}x.if t = Ax then ea otherwise eb) Ax) BY isaxiomCases x t u v () H \mvdash{} 0 \mleq{} eval x = t in 0 H \mvdash{} t \mmember{} Base H x:(t \msim{} Ax) \mvdash{} C ext ea H x:(\mforall{}[u,v:Base]. (if t = Ax then u otherwise v \msim{} v)) \mvdash{} C ext eb Date html generated: 2019_06_20-PM-04_12_13 Last ObjectModification: 2016_07_08-PM-03_48_54 Theory : rules Home Index