Nuprl Rule : equalityUniverse
This rule proved as lemma rule_equality_universe_true3 in file rules/rules_equality6.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ A1 = A2 ∈ Type
  BY equalityUniverse x1 y1 x2 y2 ()
  
  H  ⊢ (x1 = y1 ∈ A1) = (x2 = y2 ∈ A2) ∈ Type
Definitions occuring in rule : 
universe: Type
, 
equal: s = t ∈ T
, 
axiom: Ax
Latex:
H    \mvdash{}  A1  =  A2
    BY  equalityUniverse  x1  y1  x2  y2  ()
   
    H    \mvdash{}  (x1  =  y1)  =  (x2  =  y2)
Date html generated:
2019_06_20-PM-04_11_52
Last ObjectModification:
2016_07_08-PM-03_48_59
Theory : rules
Home
Index