Nuprl Lemma : sub-bag-append-trivial1
∀[T:Type]. ∀[b,x:bag(T)]. ∀y:bag(T). (sub-bag(T;b;x) ⇒ sub-bag(T;b;x + y))
Proof
Definitions occuring in Statement :
sub-bag: sub-bag(T;as;bs),
bag-append: as + bs,
bag: bag(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
sub-bag: sub-bag(T;as;bs),
exists: ∃x:A. B[x],
member: t ∈ T,
top: Top,
prop: ℙ
Lemmas referenced :
bag-append_wf,
bag-append-assoc,
istype-void,
equal_wf,
bag_wf,
sub-bag_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
sqequalHypSubstitution,
productElimination,
thin,
dependent_pairFormation_alt,
cut,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
hypothesis,
sqequalRule,
isect_memberEquality_alt,
voidElimination,
hyp_replacement,
equalitySymmetry,
applyLambdaEquality,
equalityIstype,
because_Cache,
universeIsType,
inhabitedIsType,
instantiate,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[b,x:bag(T)]. \mforall{}y:bag(T). (sub-bag(T;b;x) {}\mRightarrow{} sub-bag(T;b;x + y))
Date html generated:
2019_10_15-AM-11_01_02
Last ObjectModification:
2018_11_30-AM-10_05_07
Theory : bags
Home
Index