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