Nuprl Rule : productElimination
This rule proved as lemma rule_product_elimination_true in file rules/rules_product.v
 at https://github.com/vrahli/NuprlInCoq  
H z:(x:A × B), J ⊢ T ext let u,v = z in t
  BY productElimination #$i u v
  
  H z:(x:A × B), u:A, v:B[u/x], 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),  J  \mvdash{}  T  ext  let  u,v  =  z  in  t
    BY  productElimination  \#\$i  u  v
   
    H  z:(x:A  \mtimes{}  B),  u:A,  v:B[u/x],  J[<u,  v>/z]  \mvdash{}  T[<u,  v>/z]  ext  t
Date html generated:
2019_06_20-PM-04_11_41
Last ObjectModification:
2018_08_24-PM-04_28_48
Theory : rules
Home
Index