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: s = t ∈ T, universe: Type, axiom: Ax

Latex:
H \mvdash{} \mBbbU{}\{j\} = \mBbbU{}\{j\} BY universeEquality () CallLisp(LE-UNIVERSE-EQUALITY) No Subgoals Date html generated: 2019_06_20-PM-04_11_43 Last ObjectModification: 2016_07_08-PM-03_48_45 Theory : rules Home Index