Nuprl Lemma : cons-proper-iseg

[T:Type]. ∀L1,L2:T List. ∀a,b:T.  ([a L1] < [b L2] ⇐⇒ L1 < L2 ∧ (a b ∈ T))


Proof




Definitions occuring in Statement :  proper-iseg: L1 < L2 cons: [a b] list: List uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  proper-iseg: L1 < L2 uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q not: ¬A false: False member: t ∈ T squash: T prop: true: True rev_implies:  Q top: Top
Lemmas referenced :  iff_wf cons_iseg tl_wf reduce_tl_cons_lemma not_wf iseg_wf and_wf list_wf equal_wf true_wf squash_wf cons_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation cut independent_pairFormation sqequalHypSubstitution productElimination thin hypothesis independent_functionElimination applyEquality lambdaEquality imageElimination lemma_by_obid isectElimination hypothesisEquality equalityTransitivity equalitySymmetry because_Cache natural_numberEquality imageMemberEquality baseClosed voidElimination dependent_functionElimination isect_memberEquality voidEquality dependent_set_memberEquality setElimination rename setEquality addLevel impliesFunctionality andLevelFunctionality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.  \mforall{}a,b:T.    ([a  /  L1]  <  [b  /  L2]  \mLeftarrow{}{}\mRightarrow{}  L1  <  L2  \mwedge{}  (a  =  b))



Date html generated: 2016_05_14-PM-03_04_07
Last ObjectModification: 2016_01_15-AM-07_23_17

Theory : list_1


Home Index