---

Step * 2 1 1 of Lemma pairwise-append


1. [T] : Type
2. u : T@i
3. v : T List@i
4. ∀L2:T List
     ∀[P:T ⟶ T ⟶ ℙ']
       ((∀x,y∈v @ L2.  P[x;y]) ⇐⇒ ((∀x,y∈v.  P[x;y]) ∧ (∀x,y∈L2.  P[x;y])) ∧ (∀x∈v.(∀y∈L2.P[x;y])))@i 2
5. L2 : T List@i
6. [P] : T ⟶ T ⟶ ℙ'
⊢ (∀x,y∈v @ L2.  P[x;y]) ∧ (∀y∈v @ L2.P[u;y])
⇐⇒ (((∀x,y∈v.  P[x;y]) ∧ (∀y∈v.P[u;y])) ∧ (∀x,y∈L2.  P[x;y])) ∧ (∀y∈L2.P[u;y]) ∧ (∀x∈v.(∀y∈L2.P[x;y]))
BY
{ ((RWO "l_all_append" 0 THENA Auto) THEN RWO "-3" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T@i
3.  v  :  T  List@i
4.  \mforall{}L2:T  List
          \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}']
              ((\mforall{}x,y\mmember{}v  @  L2.    P[x;y])
              \mLeftarrow{}{}\mRightarrow{}  ((\mforall{}x,y\mmember{}v.    P[x;y])  \mwedge{}  (\mforall{}x,y\mmember{}L2.    P[x;y]))  \mwedge{}  (\mforall{}x\mmember{}v.(\mforall{}y\mmember{}L2.P[x;y])))@i  2
5.  L2  :  T  List@i
6.  [P]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}'
\mvdash{}  (\mforall{}x,y\mmember{}v  @  L2.    P[x;y])  \mwedge{}  (\mforall{}y\mmember{}v  @  L2.P[u;y])
\mLeftarrow{}{}\mRightarrow{}  (((\mforall{}x,y\mmember{}v.    P[x;y])  \mwedge{}  (\mforall{}y\mmember{}v.P[u;y]))  \mwedge{}  (\mforall{}x,y\mmember{}L2.    P[x;y]))
        \mwedge{}  (\mforall{}y\mmember{}L2.P[u;y])
        \mwedge{}  (\mforall{}x\mmember{}v.(\mforall{}y\mmember{}L2.P[x;y]))


By

---

Latex:
((RWO  "l\_all\_append"  0  THENA  Auto)  THEN  RWO  "-3"  0  THEN  Auto)\mcdot{}

---

Home Index