Nuprl Lemma : l_contains-eq_set-no_repeats

[T:Type]. ∀[as,bs:T List]. ∀[eq:EqDecider(T)].
  (no_repeats(T;as)) supposing (l_eqset(T;as;bs) and no_repeats(T;bs) and (||as|| ||bs|| ∈ ℤ))


Definitions occuring in Statement :  l_eqset: l_eqset(T;L1;L2) no_repeats: no_repeats(T;l) length: ||as|| list: List deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a set-equal: set-equal(T;x;y) all: x:A. B[x] l_eqset: l_eqset(T;L1;L2) sq_type: SQType(T) implies:  Q guard: {T} squash: T prop: true: True subtype_rel: A ⊆B iff: ⇐⇒ Q and: P ∧ Q uiff: uiff(P;Q)
Lemmas referenced :  remove-repeats-length-no-repeats remove-repeats-set-equal subtype_base_sq int_subtype_base equal_wf squash_wf true_wf iff_weakening_equal remove-repeats-length-no-repeats-iff l_eqset_wf no_repeats_wf length_wf deq_wf list_wf no_repeats_witness
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality independent_isectElimination hypothesis because_Cache instantiate cumulativity intEquality dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination applyEquality lambdaEquality imageElimination natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality productElimination isect_memberFormation isect_memberEquality

\mforall{}[T:Type].  \mforall{}[as,bs:T  List].  \mforall{}[eq:EqDecider(T)].
    (no\_repeats(T;as))  supposing  (l\_eqset(T;as;bs)  and  no\_repeats(T;bs)  and  (||as||  =  ||bs||))

Date html generated: 2017_04_17-AM-09_12_51
Last ObjectModification: 2017_02_27-PM-05_19_34

Theory : decidable!equality

Home Index