Nuprl Lemma : base_wf
Base ∈ Type
Proof
Definitions occuring in Statement :
member: t ∈ T,
base: Base,
universe: Type
Definitions unfolded in proof :
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
baseEquality
Latex:
Base \mmember{} Type
Date html generated:
2019_06_20-AM-11_13_33
Last ObjectModification:
2018_10_16-PM-04_29_25
Theory : core_2
Home
Index