Nuprl Rule : unionElimination

This rule proved as lemma rule_union_elimination_true in file rules/rules_union.v

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

  BY unionElimination #$i y
  z:(A B), x:A, J[inl x/z] ⊢ T[inl x/z] ext left
  z:(A B), y:B, 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 

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