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: List uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q sub-mset: sub-mset(T; L1; L2) exists: x:A. B[x] member: t ∈ T prop: top: Top uimplies: 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