Nuprl Lemma : empty-nat-missing_wf
empty-nat-missing() ∈ nat-missing-type()
Proof
Definitions occuring in Statement :
empty-nat-missing: empty-nat-missing(),
nat-missing-type: nat-missing-type(),
member: t ∈ T
Definitions unfolded in proof :
empty-nat-missing: empty-nat-missing(),
nat-missing-type: nat-missing-type(),
member: t ∈ T,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
implies: P ⇒ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
cand: A c∧ B,
so_lambda: λ2x y.t[x; y],
nat: ℕ,
so_apply: x[s1;s2],
so_lambda: λ2x.t[x],
top: Top,
so_apply: x[s]
Latex:
empty-nat-missing() \mmember{} nat-missing-type()
Date html generated:
2016_05_17-PM-01_45_00
Last ObjectModification:
2015_12_28-PM-08_52_09
Theory : datatype-signatures
Home
Index