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