Nuprl Lemma : rec-value_wf

rec-value() ∈ Type


Proof




Definitions occuring in Statement :  rec-value: rec-value() member: t ∈ T universe: Type
Definitions unfolded in proof :  rec-value: rec-value() member: t ∈ T uall: [x:A]. B[x] uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  co-value_wf has-value_wf-partial nat_wf set-value-type le_wf int-value-type co-value-height_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep setEquality cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin independent_isectElimination intEquality lambdaEquality natural_numberEquality hypothesisEquality

Latex:
rec-value()  \mmember{}  Type



Date html generated: 2016_05_14-PM-03_20_51
Last ObjectModification: 2015_12_26-PM-02_27_00

Theory : rec_values


Home Index