---

Step * of Lemma pairwise-mapl-no-repeats

∀[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] supposing ¬(x = y ∈ T))) ⇒ (∀x,y∈mapl(f;L).  P[x;y]) 
      supposing no_repeats(T;L)
BY
{ (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'
       (Ext2 THEN (D (-1)) THEN Auto THEN MemTypeCD THEN Auto THEN RWO "cons_member" 0 THEN Auto THEN OrRight THEN Auto)
   ⋅
   THEN Auto
   THEN Try ((Auto THEN Try (Trivial) THEN ProveListMember THEN Auto'))) }

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

2
1. [T] : Type
2. [T'] : Type
3. u : T
4. v : T List
5. ∀f:{x:T| (x ∈ v)}  ⟶ T'
     ∀[P:T' ⟶ T' ⟶ ℙ']
       (∀x,y:T.  ((x ∈ v) ⇒ (y ∈ v) ⇒ P[f x;f y] supposing ¬(x = y ∈ T))) ⇒ (∀x,y∈mapl(f;v).  P[x;y]) 
       supposing no_repeats(T;v)
6. f : {x:T| (x ∈ [u / v])}  ⟶ T'
7. [P] : T' ⟶ T' ⟶ ℙ'
8. no_repeats(T;[u / v])
9. ∀x,y:T.  ((x ∈ [u / v]) ⇒ (y ∈ [u / v]) ⇒ P[f x;f y] supposing ¬(x = y ∈ T))
10. f ∈ {x:T| (x ∈ v)}  ⟶ T'
11. (∀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]  supposing  \mneg{}(x  =  y)))  {}\mRightarrow{}  (\mforall{}x,y\mmember{}mapl(f;L).    P[x;y]) 
            supposing  no\_repeats(T;L)


By

---

Latex:
(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'
          (Ext2
            THEN  (D  (-1))
            THEN  Auto
            THEN  MemTypeCD
            THEN  Auto
            THEN  RWO  "cons\_member"  0
            THEN  Auto
            THEN  OrRight
            THEN  Auto)\mcdot{}
  THEN  Auto
  THEN  Try  ((Auto  THEN  Try  (Trivial)  THEN  ProveListMember  THEN  Auto')))

---

Home Index