Nuprl Lemma : l-ordered-no_repeats

[T:Type]. ∀[as:T List]. ∀[R:T ⟶ T ⟶ ℙ].
  (no_repeats(T;as)) supposing (l-ordered(T;x,y.R[x;y];as) and (∀x:T. R[x;x])))


Definitions occuring in Statement :  l-ordered: l-ordered(T;x,y.R[x; y];L) no_repeats: no_repeats(T;l) list: List uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] not: ¬A function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q not: ¬A implies:  Q false: False all: x:A. B[x] prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} l-ordered: l-ordered(T;x,y.R[x; y];L)
Lemmas referenced :  no_repeats_iff equal_wf l_before_wf no_repeats_witness l-ordered_wf all_wf not_wf list_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination independent_isectElimination lambdaFormation hypothesis dependent_functionElimination cumulativity independent_functionElimination voidElimination sqequalRule lambdaEquality because_Cache isect_memberEquality equalityTransitivity equalitySymmetry applyEquality functionExtensionality functionEquality universeEquality hyp_replacement dependent_set_memberEquality independent_pairFormation applyLambdaEquality setElimination rename

\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (no\_repeats(T;as))  supposing  (l-ordered(T;x,y.R[x;y];as)  and  (\mforall{}x:T.  (\mneg{}R[x;x])))

Date html generated: 2018_05_21-PM-07_39_36
Last ObjectModification: 2017_07_26-PM-05_13_53

Theory : general

Home Index