Nuprl Lemma : free-from-atom-outl2

`∀[B,A:Type]. ∀[x:A + B]. ∀[a:Atom1].  (a#outl(x):A) supposing ((↑isl(x)) and a#x:A + B)`

Proof

Definitions occuring in Statement :  free-from-atom: `a#x:T` atom: `Atom\$n` outl: `outl(x)` assert: `↑b` isl: `isl(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` 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-outl subtype_rel_union top_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:A  +  B].  \mforall{}[a:Atom1].    (a\#outl(x):A)  supposing  ((\muparrow{}isl(x))  and  a\#x:A  +  B)

Date html generated: 2016_05_13-PM-03_21_29
Last ObjectModification: 2015_12_26-AM-09_11_57

Theory : atom_1

Home Index