---

Step * of Lemma pairwise-append

∀[T:Type]
  ∀L1,L2:T List.
    ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L1 @ L2.  P[x;y]) ⇐⇒ ((∀x,y∈L1.  P[x;y]) ∧ (∀x,y∈L2.  P[x;y])) ∧ (∀x∈L1.(∀y∈L2.P[x;y])))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. [T] : Type
⊢ ∀L2:T List
    ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L2.  P[x;y]) ⇐⇒ ((∀x,y∈[].  P[x;y]) ∧ (∀x,y∈L2.  P[x;y])) ∧ (∀x∈[].(∀y∈L2.P[x;y])))

2
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])))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L1,L2:T  List.
        \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}']
            ((\mforall{}x,y\mmember{}L1  @  L2.    P[x;y])
            \mLeftarrow{}{}\mRightarrow{}  ((\mforall{}x,y\mmember{}L1.    P[x;y])  \mwedge{}  (\mforall{}x,y\mmember{}L2.    P[x;y]))  \mwedge{}  (\mforall{}x\mmember{}L1.(\mforall{}y\mmember{}L2.P[x;y])))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index