Nuprl Lemma : rationals-value-type

value-type(ℚ)


Proof




Definitions occuring in Statement :  rationals: value-type: value-type(T)
Definitions unfolded in proof :  rationals: uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  quotient-value-type b-union_wf int_nzero_wf equal_wf bool_wf qeq_wf btrue_wf qeq-equiv bunion-value-type int-value-type product-value-type
Rules used in proof :  sqequalSubstitution sqequalRule sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality productEquality hypothesis lambdaEquality hypothesisEquality independent_isectElimination because_Cache

Latex:
value-type(\mBbbQ{})



Date html generated: 2016_05_15-PM-10_37_13
Last ObjectModification: 2015_12_27-PM-08_00_39

Theory : rationals


Home Index