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} y ()
  
  H  ⊢ a1 = a2 ∈ A
  H  ⊢ b1 = b2 ∈ B[a1/x]
  H y:A ⊢ B[y/x] = B[y/x] ∈ Type
Definitions occuring in rule : 
product: x:A × B[x]
, 
pair: <a, b>
, 
equal: s = 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:
2019_06_20-PM-04_11_57
Last ObjectModification:
2016_07_08-PM-03_49_01
Theory : rules
Home
Index