Nuprl Lemma : union-nat-missing

∀[s1,s2:nat-missing-type()]. (union-nat-missing(s1;s2) ∈ nat-missing-type())

Proof

Definitions occuring in Statement : union-nat-missing: union-nat-missing(s1;s2), nat-missing-type: nat-missing-type(), uall: ∀[x:A]. B[x], member: t ∈ T
Lemmas : le_int_wf, bool_wf, eqtt_to_assert, assert_of_le_int, union-nat-missing-pos_wf, le_wf, nat-missing-type_wf
\mforall{}[s1,s2:nat-missing-type()]. (union-nat-missing(s1;s2) \mmember{} nat-missing-type()) Date html generated: 2015_07_17-AM-08_21_37 Last ObjectModification: 2015_04_02-PM-05_43_22 Home Index