### Nuprl Lemma : no_repeats-before-equality

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

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` prop: `ℙ` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` or: `P ∨ Q` not: `¬A` false: `False` uiff: `uiff(P;Q)` guard: `{T}` cand: `A 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

Latex:
\mforall{}[T:Type]
\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
no\_repeats(T;as))

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

Theory : general

Home Index