Nuprl Lemma : no_repeats-concat

[T:Type]. ∀[ll:T List List].
  (no_repeats(T;concat(ll))) supposing ((∀l∈ll.no_repeats(T;l)) and (∀l1,l2∈ll.  l_disjoint(T;l1;l2)))


Definitions occuring in Statement :  pairwise: (∀x,y∈L.  P[x; y]) l_disjoint: l_disjoint(T;l1;l2) l_all: (∀x∈L.P[x]) no_repeats: no_repeats(T;l) concat: concat(ll) list: List 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 uiff: uiff(P;Q) and: P ∧ Q cand: c∧ B implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  no_repeats-concat-iff no_repeats_witness concat_wf l_all_wf list_wf no_repeats_wf l_member_wf pairwise_wf2 l_disjoint_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination independent_isectElimination hypothesis independent_pairFormation independent_functionElimination sqequalRule lambdaEquality setElimination rename setEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry instantiate cumulativity universeEquality

\mforall{}[T:Type].  \mforall{}[ll:T  List  List].
    (no\_repeats(T;concat(ll)))  supposing 
          ((\mforall{}l\mmember{}\_repeats(T;l))  and 
          (\mforall{}l1,l2\mmember{}ll.    l\_disjoint(T;l1;l2)))

Date html generated: 2016_05_14-PM-02_55_14
Last ObjectModification: 2015_12_26-PM-02_31_32

Theory : list_1

Home Index