Nuprl Lemma : iseg_transitivity

[T:Type]. ∀l1,l2,l3:T List.  (l1 ≤ l2  l2 ≤ l3  l1 ≤ l3)


Proof




Definitions occuring in Statement :  iseg: l1 ≤ l2 list: List uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  iseg: l1 ≤ l2 uall: [x:A]. B[x] all: x:A. B[x] implies:  Q exists: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] true: True top: Top squash: T subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  append_wf equal_wf list_wf exists_wf append_assoc squash_wf true_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation sqequalHypSubstitution productElimination thin dependent_pairFormation cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis lambdaEquality Error :universeIsType,  universeEquality because_Cache natural_numberEquality isect_memberEquality voidElimination voidEquality applyEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed instantiate independent_isectElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}l1,l2,l3:T  List.    (l1  \mleq{}  l2  {}\mRightarrow{}  l2  \mleq{}  l3  {}\mRightarrow{}  l1  \mleq{}  l3)



Date html generated: 2019_06_20-PM-01_28_06
Last ObjectModification: 2018_09_26-PM-05_37_19

Theory : list_1


Home Index