Nuprl Lemma : free-from-atom-l_member

[T:Type]. ∀[L:T List]. ∀[a:Atom1]. ∀[x:T].  (a#x:T) supposing (a#L:T List and (x ∈ L))


Definitions occuring in Statement :  l_member: (x ∈ l) list: List free-from-atom: a#x:T atom: Atom$n uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a l_member: (x ∈ l) exists: x:A. B[x] cand: c∧ B prop: nat: all: x:A. B[x] sq_stable: SqStable(P) implies:  Q squash: T so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  free-from-atom_wf list_wf l_member_wf less_than_wf length_wf nat_wf select_wf sq_stable__le set_wf free-from-atom-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin equalityElimination hypothesis hyp_replacement equalitySymmetry Error :applyLambdaEquality,  extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule freeFromAtomAxiom isect_memberEquality because_Cache equalityTransitivity atomnEquality universeEquality dependent_set_memberEquality setElimination rename freeFromAtomApplication freeFromAtomTriviality lambdaEquality lambdaFormation independent_isectElimination natural_numberEquality independent_functionElimination imageMemberEquality baseClosed imageElimination freeFromAtomSet

\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[a:Atom1].  \mforall{}[x:T].    (a\#x:T)  supposing  (a\#L:T  List  and  (x  \mmember{}  L))

Date html generated: 2016_10_21-AM-09_48_32
Last ObjectModification: 2016_07_12-AM-05_08_32

Theory : list_0

Home Index