### Nuprl Lemma : union-contains2

`∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List.  bs ⊆ as ⋃ bs`

Proof

Definitions occuring in Statement :  l-union: `as ⋃ bs` l_contains: `A ⊆ B` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` l_contains: `A ⊆ B` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` guard: `{T}` or: `P ∨ Q`
Lemmas referenced :  l_all_iff l_member_wf l-union_wf member-union list_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule lambdaEquality setElimination rename hypothesis setEquality productElimination independent_functionElimination because_Cache inrFormation universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.    bs  \msubseteq{}  as  \mcup{}  bs

Date html generated: 2019_06_20-PM-01_55_04
Last ObjectModification: 2018_08_24-PM-11_26_42

Theory : decidable!equality

Home Index