### Nuprl Lemma : l-ordered-eq-rels

`∀T:Type. ∀R1,R2:T ⟶ T ⟶ ℙ. ∀L:T List.`
`  ((∀x∈L.(∀y∈L.R1[x;y] `⇐⇒` R2[x;y])) `` l-ordered(T;x,y.R1[x;y];L) `` l-ordered(T;x,y.R2[x;y];L))`

Proof

Definitions occuring in Statement :  l-ordered: `l-ordered(T;x,y.R[x; y];L)` l_all: `(∀x∈L.P[x])` list: `T List` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` l-ordered: `l-ordered(T;x,y.R[x; y];L)` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` prop: `ℙ` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]`
Lemmas referenced :  l_all_iff l_all_wf2 iff_wf l_member_wf l_before_member2 l_before_member l_before_wf l-ordered_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution cut hypothesis dependent_functionElimination thin hypothesisEquality independent_functionElimination lemma_by_obid isectElimination because_Cache sqequalRule lambdaEquality applyEquality setElimination rename setEquality productElimination allFunctionality promote_hyp functionEquality cumulativity universeEquality

Latex:
\mforall{}T:Type.  \mforall{}R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}L:T  List.
((\mforall{}x\mmember{}L.(\mforall{}y\mmember{}L.R1[x;y]  \mLeftarrow{}{}\mRightarrow{}  R2[x;y]))  {}\mRightarrow{}  l-ordered(T;x,y.R1[x;y];L)  {}\mRightarrow{}  l-ordered(T;x,y.R2[x;y];L))

Date html generated: 2016_05_15-PM-04_38_09
Last ObjectModification: 2015_12_27-PM-02_43_32

Theory : general

Home Index