Nuprl Rule : unionElimination

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

z:(A B) @lvl, J ⊢ ext case of inl(x) => left inr(y) => right

  BY unionElimination #$i y
  
  z:(A B), x:A @lvl, J[inl x/z] ⊢ T[inl x/z] ext left
  z:(A B), y:B @lvl, J[inr /z] ⊢ T[inr /z] ext right



Definitions occuring in rule :  decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x union: left right inr: inr 

Latex:
H  z:(A  +  B)  @lvl,  J  \mvdash{}  T  ext  case  z  of  inl(x)  =>  left  |  inr(y)  =>  right

    BY  unionElimination  \#\$i  x  y
   
    H  z:(A  +  B),  x:A  @lvl,  J[inl  x/z]  \mvdash{}  T[inl  x/z]  ext  left
    H  z:(A  +  B),  y:B  @lvl,  J[inr  y  /z]  \mvdash{}  T[inr  y  /z]  ext  right



Date html generated: 2016_12_14-AM-08_53_30
Last ObjectModification: 2016_07_08-PM-03_48_46

Theory : rules


Home Index