Nuprl Rule : decideExceptionCases

This rule proved as lemma rule_decide_exception_cases_true in file rules/rules_decide_exception.v

H  ⊢ b ∈ T

  BY decideExceptionCases y.u z.v ()
  H  ⊢ is-exception(case of inl(y) => inr(z) => v)
  x:(t ∈ Top Top) ⊢ b ∈ T
  x:is-exception(t) ⊢ b ∈ T
  H  ⊢ t ∈ Base

Definitions occuring in rule :  decide: case of inl(x) => s[x] inr(y) => t[y] union: left right top: Top is-exception: is-exception(t) equal: t ∈ T member: t ∈ T base: Base axiom: Ax

H    \mvdash{}  a  =  b

    BY  decideExceptionCases  x  t  y.u  z.v  ()
    H    \mvdash{}  is-exception(case  t  of  inl(y)  =>  u  |  inr(z)  =>  v)
    H  x:(t  \mmember{}  Top  +  Top)  \mvdash{}  a  =  b
    H  x:is-exception(t)  \mvdash{}  a  =  b
    H    \mvdash{}  t  \mmember{}  Base

Date html generated: 2019_06_20-PM-04_11_49
Last ObjectModification: 2016_07_08-PM-03_49_01

Theory : rules

Home Index