Nuprl Rule : unionElimination
This rule proved as lemma rule_union_elimination_true in file rules/rules_union.v
 at https://github.com/vrahli/NuprlInCoq  
H z:(A + B), J ⊢ T ext case z of inl(x) => left | inr(y) => right
  BY unionElimination #$i x y
  
  H z:(A + B), x:A, J[inl x/z] ⊢ T[inl x/z] ext left
  H z:(A + B), y:B, J[inr y /z] ⊢ T[inr y /z] ext right
Definitions occuring in rule : 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
inl: inl x
, 
union: left + right
, 
inr: inr x 
Latex:
H  z:(A  +  B),  J  \mvdash{}  T  ext  case  z  of  inl(x)  =>  left  |  inr(y)  =>  right
    BY  unionElimination  \#\$i  x  y
   
    H  z:(A  +  B),  x:A,  J[inl  x/z]  \mvdash{}  T[inl  x/z]  ext  left
    H  z:(A  +  B),  y:B,  J[inr  y  /z]  \mvdash{}  T[inr  y  /z]  ext  right
Date html generated:
2019_06_20-PM-04_11_49
Last ObjectModification:
2018_08_24-PM-04_27_03
Theory : rules
Home
Index