---

Step * 1 of Lemma pairwise-append


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])))
BY
{ ((Assert [] ∈ T List BY Auto) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  []  \mmember{}  T  List  BY  Auto)  THEN  Auto)

---

Home Index