Nuprl Rule : universeEquality

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

H  ⊢ 𝕌{j} = 𝕌{j} ∈ Type

  BY universeEquality ()
     
     CallLisp(LE-UNIVERSE-EQUALITY)
  No Subgoals



Definitions occuring in rule :  equal: t ∈ T universe: Type axiom: Ax

Latex:
H    \mvdash{}  \mBbbU{}\{j\}  =  \mBbbU{}\{j\}

    BY  universeEquality  ()
         
          CallLisp(LE-UNIVERSE-EQUALITY)
    No  Subgoals



Date html generated: 2016_12_14-AM-08_53_25
Last ObjectModification: 2016_07_08-PM-03_48_45

Theory : rules


Home Index