Nuprl Lemma : no_repeats-before-equality

  ∀as,bs:T List.
    (as bs ∈ (T List)
       ⇐⇒ (∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))) ∧ (∀x,y:T.  (x before y ∈ as ⇐⇒ before y ∈ bs))) supposing 
       (no_repeats(T;bs) and 


Definitions occuring in Statement :  l_before: before y ∈ l no_repeats: no_repeats(T;l) l_member: (x ∈ l) list: List uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] uimplies: supposing a member: t ∈ T implies:  Q iff: ⇐⇒ Q and: P ∧ Q prop: rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] or: P ∨ Q not: ¬A false: False uiff: uiff(P;Q) guard: {T} cand: c∧ B squash: T true: True
Lemmas referenced :  no_repeats_witness and_wf equal_wf list_wf l_member_wf l_before_wf all_wf iff_wf no_repeats_wf list_induction nil_wf equal-wf-base-T cons_wf cons_member null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse nil_member no_repeats_cons cons_before or_wf l_before_member l_before_member2 squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis rename because_Cache independent_pairFormation addLevel hyp_replacement equalitySymmetry sqequalRule dependent_set_memberEquality applyLambdaEquality setElimination productElimination levelHypothesis cumulativity productEquality lambdaEquality functionEquality baseClosed dependent_functionElimination inlFormation independent_isectElimination equalityTransitivity voidElimination impliesFunctionality allFunctionality allLevelFunctionality andLevelFunctionality impliesLevelFunctionality promote_hyp inrFormation unionElimination applyEquality imageElimination universeEquality natural_numberEquality imageMemberEquality

    \mforall{}as,bs:T  List.
        (as  =  bs
              \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs)))
                      \mwedge{}  (\mforall{}x,y:T.    (x  before  y  \mmember{}  as  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  bs)))  supposing 
              (no\_repeats(T;bs)  and 

Date html generated: 2018_05_21-PM-07_39_27
Last ObjectModification: 2017_07_26-PM-05_13_44

Theory : general

Home Index