Nuprl Lemma : l_contains_append

[T:Type]. ∀A,B:T List.  A ⊆ B


Proof




Definitions occuring in Statement :  l_contains: A ⊆ B append: as bs list: List 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: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q or: P ∨ Q
Lemmas referenced :  l_all_iff l_member_wf append_wf member_append all_wf or_wf list_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 inlFormation because_Cache addLevel functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}A,B:T  List.    A  \msubseteq{}  A  @  B



Date html generated: 2019_06_20-PM-01_26_39
Last ObjectModification: 2018_08_24-PM-11_16_51

Theory : list_1


Home Index