### Nuprl Lemma : list-equal-subsume

`∀[A,B:Type]. ∀[x,y:A List].  {x = y ∈ (B List) supposing x = y ∈ (A List)} supposing {a:A| (a ∈ x)}  ⊆r B`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` list: `T List` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` guard: `{T}` set: `{x:A| B[x]} ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  guard: `{T}` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B`
Lemmas referenced :  strong-subtype-equal-lists l_member_wf strong-subtype-set3 strong-subtype-self list-subtype subtype_rel_list equal_wf list_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesisEquality hypothesis independent_isectElimination because_Cache lambdaEquality cumulativity equalityTransitivity equalitySymmetry applyEquality isect_memberEquality axiomEquality universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[x,y:A  List].    \{x  =  y  supposing  x  =  y\}  supposing  \{a:A|  (a  \mmember{}  x)\}    \msubseteq{}r  B

Date html generated: 2016_05_14-AM-07_40_51
Last ObjectModification: 2015_12_26-PM-02_51_27

Theory : list_1

Home Index