Nuprl Lemma : free-from-atom-outl

[A:Type]. ∀[x:A Top]. ∀[a:Atom1].  (a#outl(x):A) supposing ((↑isl(x)) and a#x:A Top)


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] top: Top 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 outl: outl(x) bfalse: ff false: False prop: all: x:A. B[x] implies:  Q
Lemmas referenced :  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 rename voidElimination freeFromAtomAxiom hypothesis extract_by_obid isectElimination hypothesisEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry unionEquality atomnEquality universeEquality inlEquality freeFromAtomApplication freeFromAtomTriviality lambdaEquality lambdaFormation natural_numberEquality dependent_functionElimination independent_functionElimination cumulativity

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

Date html generated: 2019_06_20-AM-11_20_23
Last ObjectModification: 2018_08_21-PM-01_52_35

Theory : atom_1

Home Index