---

Step * 2 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
⊢ ∀L2:T List
    ∀[P:T ⟶ T ⟶ ℙ']
      ((∀x,y∈[u / (v @ L2)].  P[x;y]) ⇐⇒ ((∀x,y∈[u / v].  P[x;y]) ∧ (∀x,y∈L2.  P[x;y])) ∧ (∀x∈[u / v].(∀y∈L2.P[x;y])))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
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∈[u / (v @ L2)].  P[x;y]) ⇐⇒ ((∀x,y∈[u / v].  P[x;y]) ∧ (∀x,y∈L2.  P[x;y])) ∧ (∀x∈[u / v].(∀y∈L2.P[x;y]))

---

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
\mvdash{}  \mforall{}L2:T  List
        \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}']
            ((\mforall{}x,y\mmember{}[u  /  (v  @  L2)].    P[x;y])
            \mLeftarrow{}{}\mRightarrow{}  ((\mforall{}x,y\mmember{}[u  /  v].    P[x;y])  \mwedge{}  (\mforall{}x,y\mmember{}L2.    P[x;y]))  \mwedge{}  (\mforall{}x\mmember{}[u  /  v].(\mforall{}y\mmember{}L2.P[x;y])))


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index