Nuprl Lemma : member-of-tagged+1

[T,B:Type]. ∀[tg,a:Atom]. ∀[x:T].  mk-tagged(tg;x) ∈ tg:T |+ a:B supposing ¬(tg a ∈ Atom)


Proof




Definitions occuring in Statement :  mk-tagged: mk-tagged(tg;x) tagged+: |+ z:B tag-case: z:T uimplies: supposing a uall: [x:A]. B[x] not: ¬A member: t ∈ T atom: Atom universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a tagged+: |+ z:B isect2: T1 ⋂ T2 bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) bfalse: ff subtype_rel: A ⊆B implies:  Q iff: ⇐⇒ Q not: ¬A prop: rev_implies:  Q false: False top: Top
Lemmas referenced :  mk-tagged_wf assert_of_eq_atom mk-tagged_wf_unequal iff_transitivity not_wf equal-wf-base atom_subtype_base assert_wf eq_atom_wf bnot_wf iff_weakening_uiff assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut isect_memberEquality sqequalHypSubstitution unionElimination thin equalityElimination sqequalRule extract_by_obid isectElimination hypothesisEquality because_Cache hypothesis productElimination independent_pairFormation independent_isectElimination atomEquality applyEquality independent_functionElimination lambdaFormation impliesFunctionality equalitySymmetry voidElimination voidEquality axiomEquality equalityTransitivity universeEquality

Latex:
\mforall{}[T,B:Type].  \mforall{}[tg,a:Atom].  \mforall{}[x:T].    mk-tagged(tg;x)  \mmember{}  tg:T  |+  a:B  supposing  \mneg{}(tg  =  a)



Date html generated: 2018_05_21-PM-08_43_20
Last ObjectModification: 2017_07_26-PM-06_07_15

Theory : general


Home Index