Nuprl Rule : dependent_pairFormation

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

H  ⊢ x:A × ext <a, b>

  BY dependent_pairFormation !parameter{i:l} ()
  
  H  ⊢ a ∈ A
  H  ⊢ B[a/x] ext b
  y:A ⊢ B[y/x] B[y/x] ∈ Type



Definitions occuring in rule :  product: x:A × B[x] pair: <a, b> equal: t ∈ T universe: Type axiom: Ax

Latex:
H    \mvdash{}  x:A  \mtimes{}  B  ext  <a,  b>

    BY  dependent\_pairFormation  !parameter\{i:l\}  a  y  ()
   
    H    \mvdash{}  a  =  a
    H    \mvdash{}  B[a/x]  ext  b
    H  y:A  \mvdash{}  B[y/x]  =  B[y/x]



Date html generated: 2016_12_14-AM-08_53_31
Last ObjectModification: 2016_07_08-PM-03_49_01

Theory : rules


Home Index