Nuprl Lemma : free-from-atom-outr2

[B,A:Type]. ∀[x:B A]. ∀[a:Atom1].  (a#outr(x):A) supposing ((¬↑isl(x)) and a#x:B A)


Definitions occuring in Statement :  free-from-atom: a#x:T atom: Atom$n outr: outr(x) assert: b isl: isl(x) uimplies: supposing a uall: [x:A]. B[x] not: ¬A union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uimplies: supposing a top: Top prop:
Lemmas referenced :  free-from-atom-outr subtype_rel_union top_wf not_wf assert_wf isl_wf free-from-atom_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality because_Cache independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality sqequalRule freeFromAtomApplication freeFromAtomTriviality unionEquality freeFromAtomAxiom equalityTransitivity equalitySymmetry atomnEquality universeEquality

\mforall{}[B,A:Type].  \mforall{}[x:B  +  A].  \mforall{}[a:Atom1].    (a\#outr(x):A)  supposing  ((\mneg{}\muparrow{}isl(x))  and  a\#x:B  +  A)

Date html generated: 2016_05_13-PM-03_21_32
Last ObjectModification: 2015_12_26-AM-09_11_53

Theory : atom_1

Home Index