Nuprl Lemma : l_subset_transitivity

[T:Type]. ∀A,B,C:T List.  (l_subset(T;A;B)  l_subset(T;B;C)  l_subset(T;A;C))


Proof




Definitions occuring in Statement :  l_subset: l_subset(T;as;bs) 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 member: t ∈ T prop: iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  l_contains_wf l_subset-l_contains l_subset_wf list_wf l_contains_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis addLevel impliesFunctionality dependent_functionElimination productElimination independent_functionElimination because_Cache functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}A,B,C:T  List.    (l\_subset(T;A;B)  {}\mRightarrow{}  l\_subset(T;B;C)  {}\mRightarrow{}  l\_subset(T;A;C))



Date html generated: 2016_05_14-AM-07_54_21
Last ObjectModification: 2015_12_26-PM-04_48_37

Theory : list_1


Home Index