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: 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 ⊆B uimplies: 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