Nuprl Lemma : void_wf
Void ∈ Type
Proof
Definitions occuring in Statement :
member: t ∈ T,
void: Void,
universe: Type
Definitions unfolded in proof :
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
voidEquality
Latex:
Void \mmember{} Type
Date html generated:
2019_06_20-AM-11_14_00
Last ObjectModification:
2018_10_15-AM-08_51_02
Theory : core_2
Home
Index