### Nuprl Lemma : list-is-singleton-iff

`∀[T:Type]. ∀L:T List. ∀x:T.  (L = [x] ∈ (T List) `⇐⇒` no_repeats(T;L) ∧ (∀f:T. ((f ∈ L) `⇐⇒` f = x ∈ T)))`

Proof

Definitions occuring in Statement :  no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` cons: `[a / b]` nil: `[]` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` rev_implies: `P `` Q` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` not: `¬A` false: `False` top: `Top` select: `L[n]` cons: `[a / b]` cand: `A c∧ B` less_than: `a < b` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uiff: `uiff(P;Q)` nat_plus: `ℕ+` subtract: `n - m`
Lemmas referenced :  no_repeats_witness l_member_wf cons_wf nil_wf no_repeats_wf list_wf istype-universe squash_wf true_wf subtype_rel_self iff_weakening_equal no_repeats_singleton member_singleton istype-void istype-le length_of_cons_lemma length_of_nil_lemma istype-less_than length_wf select_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf list-cases product_subtype_list null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse no_repeats_cons cons_member add_nat_plus add_nat_wf length_wf_nat decidable__lt intformless_wf int_formula_prop_less_lemma nat_plus_properties add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma false_wf non_neg_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt independent_pairFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis universeIsType equalityIstype inhabitedIsType productElimination sqequalRule productIsType functionIsType because_Cache instantiate universeEquality applyEquality lambdaEquality_alt imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed independent_isectElimination dependent_functionElimination dependent_pairFormation_alt dependent_set_memberEquality_alt voidElimination isect_memberEquality_alt setElimination rename unionElimination approximateComputation int_eqEquality promote_hyp hypothesis_subsumption inlFormation_alt applyLambdaEquality pointwiseFunctionality baseApply closedConclusion addEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    (L  =  [x]  \mLeftarrow{}{}\mRightarrow{}  no\_repeats(T;L)  \mwedge{}  (\mforall{}f:T.  ((f  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  f  =  x)))

Date html generated: 2020_05_19-PM-09_42_35
Last ObjectModification: 2019_11_13-PM-00_33_02

Theory : list_1

Home Index