### Nuprl Lemma : l_before_append_iff

`∀[T:Type]. ∀A,B:T List. ∀x,y:T.  (x before y ∈ A @ B `⇐⇒` x before y ∈ A ∨ x before y ∈ B ∨ ((x ∈ A) ∧ (y ∈ B)))`

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` l_member: `(x ∈ l)` append: `as @ bs` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  rev_implies: `P `` Q` iff: `P `⇐⇒` Q` implies: `P `` Q` so_apply: `x[s]` and: `P ∧ Q` or: `P ∨ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` guard: `{T}` uimplies: `b supposing a` not: `¬A` false: `False` cand: `A c∧ B`
Lemmas referenced :  istype-universe l_member_wf append_wf l_before_wf iff_wf list_wf list_induction list_ind_nil_lemma nil_wf or_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse nil_before cons_wf list_ind_cons_lemma istype-void cons_before cons_member member_append
Rules used in proof :  universeEquality instantiate dependent_functionElimination unionIsType productIsType because_Cache functionIsType rename independent_functionElimination universeIsType productEquality unionEquality hypothesis functionEquality lambdaEquality_alt sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution isect_memberEquality voidElimination voidEquality lambdaFormation independent_pairFormation inrFormation inlFormation cumulativity unionElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry inhabitedIsType equalityIstype isect_memberEquality_alt inlFormation_alt inrFormation_alt promote_hyp

Latex:
\mforall{}[T:Type]
\mforall{}A,B:T  List.  \mforall{}x,y:T.
(x  before  y  \mmember{}  A  @  B  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  A  \mvee{}  x  before  y  \mmember{}  B  \mvee{}  ((x  \mmember{}  A)  \mwedge{}  (y  \mmember{}  B)))

Date html generated: 2019_10_15-AM-10_21_41
Last ObjectModification: 2019_08_05-PM-02_08_48

Theory : list_1

Home Index