Nuprl Lemma : rat_termco_wf

rat_termco() ∈ Type


Proof




Definitions occuring in Statement :  rat_termco: rat_termco() member: t ∈ T universe: Type
Definitions unfolded in proof :  rat_termco: rat_termco() member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  corec_wf ifthenelse_wf eq_atom_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin lambdaEquality_alt productEquality atomEquality instantiate hypothesisEquality tokenEquality hypothesis universeEquality intEquality voidEquality

Latex:
rat\_termco()  \mmember{}  Type



Date html generated: 2019_10_29-AM-09_24_47
Last ObjectModification: 2019_03_31-PM-05_24_03

Theory : reals


Home Index