---

Step * of Lemma pairwise-map2

∀[T,T':Type].
  ∀L:T List. ∀f:{t:T| (t ∈ L)}  ⟶ T'.  ∀[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 3 (ParallelLast')
   THEN (UnivCD THENA Auto)
   THEN (InstHyp [⌜P⌝;⌜f⌝] 4⋅ THENA Auto)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T,T':Type].
    \mforall{}L:T  List.  \mforall{}f:\{t:T|  (t  \mmember{}  L)\}    {}\mrightarrow{}  T'.
        \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  3  (ParallelLast')
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  Trivial)

---

Home Index