Nuprl Rule : baseEquality
This rule proved as lemma rule_base_equality_true3 in file rules/rules_base.v at https://github.com/vrahli/NuprlInCoq
H ⊢ Base = Base ∈ Type
BY baseEquality ()
No Subgoals
Definitions occuring in rule :
equal: s = t ∈ T,
universe: Type,
base: Base,
axiom: Ax
Latex:
H \mvdash{} Base = Base
BY baseEquality ()
No Subgoals
Date html generated:
2019_06_20-PM-04_12_30
Last ObjectModification:
2016_07_08-PM-03_49_06
Theory : rules
Home
Index