Nuprl Lemma : sub-mset_transitivity
∀[T:Type]. ∀A,B,C:T List. (sub-mset(T; A; B) ⇒ sub-mset(T; B; C) ⇒ sub-mset(T; A; C))
Proof
Definitions occuring in Statement :
sub-mset: sub-mset(T; L1; L2),
list: T List,
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-mset: sub-mset(T; L1; L2),
exists: ∃x:A. B[x],
member: t ∈ T,
prop: ℙ,
top: Top,
uimplies: b supposing a
Lemmas referenced :
append_wf,
permutation_wf,
sub-mset_wf,
list_wf,
permutation_transitivity,
append_assoc_sq,
append_functionality_wrt_permutation,
permutation-rotate,
permutation_weakening
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
dependent_pairFormation,
cut,
lemma_by_obid,
isectElimination,
hypothesisEquality,
hypothesis,
universeEquality,
dependent_functionElimination,
independent_functionElimination,
because_Cache,
isect_memberEquality,
voidElimination,
voidEquality,
sqequalRule,
independent_isectElimination
Latex:
\mforall{}[T:Type]. \mforall{}A,B,C:T List. (sub-mset(T; A; B) {}\mRightarrow{} sub-mset(T; B; C) {}\mRightarrow{} sub-mset(T; A; C))
Date html generated:
2016_05_15-PM-04_32_11
Last ObjectModification:
2015_12_27-PM-02_50_02
Theory : general
Home
Index