Nuprl Lemma : list-diff_functionality
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs,cs:T List].
as-bs = as-cs ∈ (T List) supposing ∀x:T. ((x ∈ as) ⇒ ((x ∈ bs) ⇐⇒ (x ∈ cs)))
Proof
Definitions occuring in Statement :
list-diff: as-bs,
l_member: (x ∈ l),
list: T List,
deq: EqDecider(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
list-diff: as-bs,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
squash: ↓T,
subtype_rel: A ⊆r B,
not: ¬A,
false: False,
true: True,
guard: {T}
Lemmas referenced :
list-subtype,
l_member_wf,
filter_wf5,
squash_wf,
true_wf,
bool_wf,
list_wf,
istype-universe,
subtype_rel_list,
iff_imp_equal_bool,
bnot_wf,
deq-member_wf,
istype-void,
iff_transitivity,
assert_wf,
not_wf,
iff_weakening_uiff,
assert_of_bnot,
assert-deq-member,
istype-assert
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
inhabitedIsType,
lambdaFormation_alt,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
sqequalRule,
functionIsType,
universeIsType,
productIsType,
because_Cache,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
applyEquality,
lambdaEquality_alt,
imageElimination,
setIsType,
instantiate,
universeEquality,
setEquality,
independent_isectElimination,
setElimination,
rename,
independent_pairFormation,
voidElimination,
productElimination,
promote_hyp,
natural_numberEquality,
imageMemberEquality,
baseClosed,
hyp_replacement,
dependent_set_memberEquality_alt,
applyLambdaEquality
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[as,bs,cs:T List].
as-bs = as-cs supposing \mforall{}x:T. ((x \mmember{} as) {}\mRightarrow{} ((x \mmember{} bs) \mLeftarrow{}{}\mRightarrow{} (x \mmember{} cs)))
Date html generated:
2020_05_19-PM-09_52_33
Last ObjectModification:
2020_01_04-PM-08_00_00
Theory : decidable!equality
Home
Index