### 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)`

Proof

Definitions occuring in Statement :  free-from-atom: `a#x:T` atom: `Atom\$n` outr: `outr(x)` assert: `↑b` isl: `isl(x)` uimplies: `b 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 ⊆r B` uimplies: `b 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

Latex:
\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