Nuprl Rule : dependent_pairEquality

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

H  ⊢ <a1, b1> = <a2, b2> ∈ (x:A × B)

  BY dependent_pairEquality !parameter{i:l} ()
  
  H  ⊢ a1 a2 ∈ A
  H  ⊢ b1 b2 ∈ B[a1/x]
  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{}  <a1,  b1>  =  <a2,  b2>

    BY  dependent\_pairEquality  !parameter\{i:l\}  y  ()
   
    H    \mvdash{}  a1  =  a2
    H    \mvdash{}  b1  =  b2
    H  y:A  \mvdash{}  B[y/x]  =  B[y/x]



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

Theory : rules


Home Index