Nuprl Lemma : l_contains-append

[T:Type]. ∀A,B,C:T List.  (A B ⊆ ⇐⇒ A ⊆ C ∧ B ⊆ C)


Proof




Definitions occuring in Statement :  l_contains: A ⊆ B append: as bs list: List uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] l_contains: A ⊆ B iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T or: P ∨ Q prop: guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q
Lemmas referenced :  l_member_wf all_wf or_wf member_append append_wf iff_wf l_all_iff l_all_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut independent_pairFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination inlFormation introduction extract_by_obid isectElimination sqequalRule inrFormation because_Cache lambdaEquality functionEquality productElimination unionElimination productEquality addLevel setElimination rename setEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}A,B,C:T  List.    (A  @  B  \msubseteq{}  C  \mLeftarrow{}{}\mRightarrow{}  A  \msubseteq{}  C  \mwedge{}  B  \msubseteq{}  C)



Date html generated: 2019_06_20-PM-01_26_43
Last ObjectModification: 2018_08_24-PM-11_16_47

Theory : list_1


Home Index