Nuprl Lemma : name-valueall-type
valueall-type(Name)
Proof
Definitions occuring in Statement :
name: Name,
valueall-type: valueall-type(T)
Definitions unfolded in proof :
name: Name,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a
Lemmas referenced :
list-valueall-type,
atom-valueall-type
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
atomEquality,
independent_isectElimination,
hypothesis
Latex:
valueall-type(Name)
Date html generated:
2016_05_14-PM-03_33_59
Last ObjectModification:
2015_12_26-PM-06_00_45
Theory : decidable!equality
Home
Index