---

Step * of Lemma pairwise-mapl

∀[T,T':Type].
  ∀L:T List. ∀f:{x:T| (x ∈ L)}  ⟶ T'.
    ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T.  ((x ∈ L) ⇒ (y ∈ L) ⇒ P[f x;f y])) ⇒ (∀x,y∈mapl(f;L).  P[x;y]))
BY
{ TACTIC:(InductionOnList
          THEN Auto
          THEN Unfold `mapl` 0
          THEN Reduce 0
          THEN Try (Fold `mapl` 0)
          THEN Try ((RWO "pairwise-nil" 0 THEN Auto))
          THEN Try ((RWO "pairwise-cons" 0 THENA Auto))
          THEN AssertBY f ∈ {x:T| (x ∈ v)}  ⟶ T'
              Auto⋅
          THEN Auto) }

1
1. [T] : Type
2. [T'] : Type
3. u : T@i
4. v : T List@i
5. ∀f:{x:T| (x ∈ v)}  ⟶ T'
     ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T.  ((x ∈ v) ⇒ (y ∈ v) ⇒ P[f x;f y])) ⇒ (∀x,y∈mapl(f;v).  P[x;y]))
6. f : {x:T| (x ∈ [u / v])}  ⟶ T'@i
7. [P] : T' ⟶ T' ⟶ ℙ'
8. ∀x,y:T.  ((x ∈ [u / v]) ⇒ (y ∈ [u / v]) ⇒ P[f x;f y])
9. f ∈ {x:T| (x ∈ v)}  ⟶ T'
10. (∀x,y∈mapl(f;v).  P[x;y])
⊢ (∀y∈mapl(f;v).P[f u;y])

---

Latex:

---

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


By

---

Latex:
TACTIC:(InductionOnList
                THEN  Auto
                THEN  Unfold  `mapl`  0
                THEN  Reduce  0
                THEN  Try  (Fold  `mapl`  0)
                THEN  Try  ((RWO  "pairwise-nil"  0  THEN  Auto))
                THEN  Try  ((RWO  "pairwise-cons"  0  THENA  Auto))
                THEN  AssertBY  f  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'
                        Auto\mcdot{}
                THEN  Auto)

---

Home Index