---

Step * of Lemma pairwise-map1

∀[T,T':Type].  ∀f:T ⟶ T'. ∀L:T List.  ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y∈map(f;L).  P[x;y]) ⇐⇒ (∀x,y∈L.  P[f x;f y]))
BY
{ (InstLemma `pairwise-map` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (UnivCD THENA Auto)
   THEN (InstHyp [⌜L⌝;⌜P⌝;⌜f⌝] 3⋅ THENA Auto)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T,T':Type].
    \mforall{}f:T  {}\mrightarrow{}  T'.  \mforall{}L:T  List.    \mforall{}[P:T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}'].  ((\mforall{}x,y\mmember{}map(f;L).    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x,y\mmember{}L.    P[f  x;f  y]))


By

---

Latex:
(InstLemma  `pairwise-map`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  Trivial)

---

Home Index