Nuprl Lemma : free-from-atom-outr

[A:Type]. ∀[x:Top A]. ∀[a:Atom1].  (a#outr(x):A) supposing ((¬↑isl(x)) and a#x:Top 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] top: Top not: ¬A union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a isl: isl(x) assert: b ifthenelse: if then else fi  btrue: tt outr: outr(x) not: ¬A implies:  Q true: True false: False bfalse: ff prop: all: x:A. B[x]
Lemmas referenced :  not_wf assert_wf isl_wf top_wf free-from-atom_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut unionElimination thin sqequalHypSubstitution sqequalRule independent_functionElimination natural_numberEquality voidElimination rename freeFromAtomAxiom hypothesis extract_by_obid isectElimination hypothesisEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry unionEquality atomnEquality universeEquality inrEquality freeFromAtomApplication freeFromAtomTriviality lambdaEquality lambdaFormation dependent_functionElimination cumulativity

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

Date html generated: 2019_06_20-AM-11_20_25
Last ObjectModification: 2018_08_21-PM-01_52_37

Theory : atom_1

Home Index