Nuprl Rule : isectEquality
This rule proved as lemma rule_isect_equality_true3 in file rules/rules_isect.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ (⋂x1:a1. b1) = (⋂x2:a2. b2) ∈ Type
  BY isectEquality y ()
  
  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type
Definitions occuring in rule : 
isect: ⋂x:A. B[x]
, 
equal: s = t ∈ T
, 
universe: Type
, 
axiom: Ax
Latex:
H    \mvdash{}  (\mcap{}x1:a1.  b1)  =  (\mcap{}x2:a2.  b2)
    BY  isectEquality  y  ()
   
    H    \mvdash{}  a1  =  a2
    H  y:a1  \mvdash{}  b1[y/x1]  =  b2[y/x2]
Date html generated:
2019_06_20-PM-04_11_52
Last ObjectModification:
2016_07_08-PM-03_48_54
Theory : rules
Home
Index