Nuprl Lemma : atomic-values_subtype_base

atomic-values() ⊆Base


Proof




Definitions occuring in Statement :  atomic-values: atomic-values() subtype_rel: A ⊆B base: Base
Definitions unfolded in proof :  subtype_rel: A ⊆B member: t ∈ T atomic-values: atomic-values() Value: Value()
Lemmas referenced :  atomic-values_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality cut lemma_by_obid hypothesis

Latex:
atomic-values()  \msubseteq{}r  Base



Date html generated: 2016_05_13-PM-03_23_05
Last ObjectModification: 2015_12_26-AM-09_30_53

Theory : call!by!value_1


Home Index