---

Step * 1 1 1 1 1 1 1 4 of Lemma alpha-rename-equivalent

.....antecedent..... 
1. v : varname()
2. bnds : varname() List
⊢ ∀aaaa:varname(). ∀LLLL:varname() List.
    ((∀F:{v@0:varname()| (v@0 ∈ LLLL)}  ⟶ varname()
        ((v ∈ LLLL) ⇒ Inj({v@0:varname()| (v@0 ∈ LLLL)} ;varname();F) ⇒ (↑same-binding(map(F;LLLL);LLLL;F v;v))))
    ⇒ (∀F:{v@0:varname()| (v@0 ∈ [aaaa / LLLL])}  ⟶ varname()
          ((v ∈ [aaaa / LLLL])
          ⇒ Inj({v@0:varname()| (v@0 ∈ [aaaa / LLLL])} ;varname();F)
          ⇒ (↑same-binding(map(F;[aaaa / LLLL]);[aaaa / LLLL];F v;v)))))
BY
{ (All Thin
   THEN RepeatFor 2 (Intro)
   THEN RenameVar `u' (-2)
   THEN RenameVar `bnds' (-1)
   THEN (Assert bnds ∈ {v:varname()| (v ∈ bnds)}  List BY
               Auto)
   THEN Intros) }

1
1. v : varname()
2. u : varname()
3. bnds : varname() List
4. bnds ∈ {v:varname()| (v ∈ bnds)}  List
5. ∀F:{v@0:varname()| (v@0 ∈ bnds)}  ⟶ varname()
     ((v ∈ bnds) ⇒ Inj({v@0:varname()| (v@0 ∈ bnds)} ;varname();F) ⇒ (↑same-binding(map(F;bnds);bnds;F v;v)))
6. F : {v@0:varname()| (v@0 ∈ [u / bnds])}  ⟶ varname()
7. (v ∈ [u / bnds])
8. Inj({v@0:varname()| (v@0 ∈ [u / bnds])} ;varname();F)
⊢ ↑same-binding(map(F;[u / bnds]);[u / bnds];F v;v)

---

Latex:

---

Latex:
.....antecedent..... 
1.  v  :  varname()
2.  bnds  :  varname()  List
\mvdash{}  \mforall{}aaaa:varname().  \mforall{}LLLL:varname()  List.
        ((\mforall{}F:\{v@0:varname()|  (v@0  \mmember{}  LLLL)\}    {}\mrightarrow{}  varname()
                ((v  \mmember{}  LLLL)
                {}\mRightarrow{}  Inj(\{v@0:varname()|  (v@0  \mmember{}  LLLL)\}  ;varname();F)
                {}\mRightarrow{}  (\muparrow{}same-binding(map(F;LLLL);LLLL;F  v;v))))
        {}\mRightarrow{}  (\mforall{}F:\{v@0:varname()|  (v@0  \mmember{}  [aaaa  /  LLLL])\}    {}\mrightarrow{}  varname()
                    ((v  \mmember{}  [aaaa  /  LLLL])
                    {}\mRightarrow{}  Inj(\{v@0:varname()|  (v@0  \mmember{}  [aaaa  /  LLLL])\}  ;varname();F)
                    {}\mRightarrow{}  (\muparrow{}same-binding(map(F;[aaaa  /  LLLL]);[aaaa  /  LLLL];F  v;v)))))


By

---

Latex:
(All  Thin
  THEN  RepeatFor  2  (Intro)
  THEN  RenameVar  `u'  (-2)
  THEN  RenameVar  `bnds'  (-1)
  THEN  (Assert  bnds  \mmember{}  \{v:varname()|  (v  \mmember{}  bnds)\}    List  BY
                          Auto)
  THEN  Intros)

---

Home Index