Nuprl Rule : productElimination

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

z:(x:A × B) @lvl, J ⊢ ext let u,v in t

  BY productElimination #$i v
  
  z:(x:A × B), u:A @lvl, v:B[u/x] @lvl, J[<u, v>/z] ⊢ T[<u, v>/z] ext t



Definitions occuring in rule :  spread: spread def product: x:A × B[x] pair: <a, b>

Latex:
H  z:(x:A  \mtimes{}  B)  @lvl,  J  \mvdash{}  T  ext  let  u,v  =  z  in  t

    BY  productElimination  \#\$i  u  v
   
    H  z:(x:A  \mtimes{}  B),  u:A  @lvl,  v:B[u/x]  @lvl,  J[<u,  v>/z]  \mvdash{}  T[<u,  v>/z]  ext  t



Date html generated: 2016_12_14-AM-08_53_24
Last ObjectModification: 2016_07_08-PM-03_48_49

Theory : rules


Home Index