Nuprl Rule : isinrCases
This rule proved as lemma rule_isinr_cases_true in file rules/rules_inl_inr_cases.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ C ext !((!\\x.if t is inr then ea else eb) Ax)
  BY isinrCases x t u v ()
  
  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ inr outr(t) ) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is inr then u else v ~ v)) ⊢ C ext eb
Definitions occuring in rule : 
sqle: s ≤ t
, 
callbyvalue: callbyvalue, 
natural_number: $n
, 
member: t ∈ T
, 
axiom: Ax
, 
inr: inr x 
, 
outr: outr(x)
, 
uall: ∀[x:A]. B[x]
, 
base: Base
, 
sqequal: s ~ t
, 
isinr: isinr def
Latex:
H    \mvdash{}  C  ext  !((!\mbackslash{}\mbackslash{}x.if  t  is  inr  then  ea  else  eb)  Ax)
    BY  isinrCases  x  t  u  v  ()
   
    H    \mvdash{}  0  \mleq{}  eval  x  =  t  in  0
    H    \mvdash{}  t  \mmember{}  Base
    H  x:(t  \msim{}  inr  outr(t)  )  \mvdash{}  C  ext  ea
    H  x:(\mforall{}[u,v:Base].    (if  t  is  inr  then  u  else  v  \msim{}  v))  \mvdash{}  C  ext  eb
Date html generated:
2019_06_20-PM-04_12_10
Last ObjectModification:
2016_07_08-PM-03_48_53
Theory : rules
Home
Index