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