Nuprl Lemma : nullvar_wf
nullvar() ∈ varname()
Proof
Definitions occuring in Statement :
nullvar: nullvar(),
varname: varname(),
member: t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
nullvar: nullvar(),
subtype_rel: A ⊆r B
Lemmas referenced :
atom_subtype_varname
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
tokenEquality,
applyEquality,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution
Latex:
nullvar() \mmember{} varname()
Date html generated:
2020_05_19-PM-09_53_19
Last ObjectModification:
2020_03_09-PM-04_08_04
Theory : terms
Home
Index