---

Step * 2 of Lemma pairwise-mapl-no-repeats


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])
BY
{ (D 0
   THEN Auto
   THEN (InstLemma `member-mapl` [⌜T⌝;⌜T'⌝;⌜v⌝;⌜mapl(f;v)[i]⌝;⌜f⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN (D -2 THENA Auto)
   THEN ExRepD
   THEN Thin 10
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN BackThruSomeHyp
   THEN Auto
   THEN OnMaybeHyp 8 (\h. ((RWO "no_repeats_cons" h THENA Auto) THEN Auto THEN ParallelOp (h+1) THEN Auto))) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [T']  :  Type
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}f:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'
          \mforall{}[P:T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}']
              (\mforall{}x,y:T.    ((x  \mmember{}  v)  {}\mRightarrow{}  (y  \mmember{}  v)  {}\mRightarrow{}  P[f  x;f  y]  supposing  \mneg{}(x  =  y)))
              {}\mRightarrow{}  (\mforall{}x,y\mmember{}mapl(f;v).    P[x;y]) 
              supposing  no\_repeats(T;v)
6.  f  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  T'
7.  [P]  :  T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}'
8.  no\_repeats(T;[u  /  v])
9.  \mforall{}x,y:T.    ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  (y  \mmember{}  [u  /  v])  {}\mRightarrow{}  P[f  x;f  y]  supposing  \mneg{}(x  =  y))
10.  f  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'
11.  (\mforall{}x,y\mmember{}mapl(f;v).    P[x;y])
\mvdash{}  (\mforall{}y\mmember{}mapl(f;v).P[f  u;y])


By

---

Latex:
(D  0
  THEN  Auto
  THEN  (InstLemma  `member-mapl`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}T'\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}mapl(f;v)[i]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  (D  -2  THENA  Auto)
  THEN  ExRepD
  THEN  Thin  10
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  OnMaybeHyp  8  (\mbackslash{}h.  ((RWO  "no\_repeats\_cons"  h  THENA  Auto)
                                                  THEN  Auto
                                                  THEN  ParallelOp  (h+1)
                                                  THEN  Auto)))

---

Home Index