Nuprl Lemma : no_repeats-sublist

[T:Type]. ∀[L,L':T List].  (no_repeats(T;L')) supposing (L' ⊆ and no_repeats(T;L))


Definitions occuring in Statement :  sublist: L1 ⊆ L2 no_repeats: no_repeats(T;l) list: List uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T not: ¬A implies:  Q false: False prop: so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q guard: {T} all: x:A. B[x]
Lemmas referenced :  equal_wf l_before_wf sublist_wf uall_wf isect_wf not_wf iff_weakening_uiff no_repeats_wf no_repeats_iff no_repeats_witness list_wf l_before_sublist
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination extract_by_obid isectElimination hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination because_Cache isect_memberEquality equalityTransitivity equalitySymmetry addLevel independent_isectElimination productElimination cumulativity isectEquality universeEquality

\mforall{}[T:Type].  \mforall{}[L,L':T  List].    (no\_repeats(T;L'))  supposing  (L'  \msubseteq{}  L  and  no\_repeats(T;L))

Date html generated: 2019_06_20-PM-01_27_21
Last ObjectModification: 2018_08_24-PM-11_25_48

Theory : list_1

Home Index