Nuprl Lemma : no_repeats_witness

[T:Type]. ∀[l:T List].  (no_repeats(T;l)  x.Ax ∈ no_repeats(T;l)))


Proof




Definitions occuring in Statement :  no_repeats: no_repeats(T;l) list: List uall: [x:A]. B[x] implies:  Q member: t ∈ T lambda: λx.A[x] universe: Type axiom: Ax
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q no_repeats: no_repeats(T;l) uimplies: supposing a not: ¬A false: False nat: sq_stable: SqStable(P) squash: T prop:
Lemmas referenced :  equal_wf select_wf sq_stable__le not_wf nat_wf less_than_wf length_wf no_repeats_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality lambdaEquality dependent_functionElimination voidElimination extract_by_obid cumulativity because_Cache setElimination rename hypothesis independent_isectElimination natural_numberEquality independent_functionElimination imageMemberEquality baseClosed imageElimination equalityTransitivity equalitySymmetry axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].    (no\_repeats(T;l)  {}\mRightarrow{}  (\mlambda{}x.Ax  \mmember{}  no\_repeats(T;l)))



Date html generated: 2017_04_14-AM-08_37_35
Last ObjectModification: 2017_02_27-PM-03_29_19

Theory : list_0


Home Index