---

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


1. v : varname()
2. bnds : varname() List
⊢ ∀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)))
BY
{ (InstLemma `list_induction` [⌜varname()⌝;⌜λ2bnds.∀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)))⌝;⌜bnds⌝]⋅
   THEN Try (Trivial)
   ) }

1
.....wf..... 
1. v : varname()
2. bnds : varname() List
⊢ varname() ∈ Type

2
.....wf..... 
1. v : varname()
2. bnds : varname() List
⊢ λbnds.∀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)))
  ∈ (varname() List) ⟶ ℙ

3
.....antecedent..... 
1. v : varname()
2. bnds : varname() List
⊢ ∀F:{v@0:varname()| (v@0 ∈ [])}  ⟶ varname()
    ((v ∈ []) ⇒ Inj({v@0:varname()| (v@0 ∈ [])} ;varname();F) ⇒ (↑same-binding(map(F;[]);[];F v;v)))

4
.....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)))))

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `list\_induction`  [\mkleeneopen{}varname()\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bnds.\mforall{}F:\{v@0:varname()|  (v@0  \mmember{}  bnds)\}    {}\mrightarrow{}  varname()
                                                                                                      ((v  \mmember{}  bnds)
                                                                                                      {}\mRightarrow{}  Inj(\{v@0:varname()|  (v@0  \mmember{}  bnds)\}  ;varname();F\000C)
                                                                                                      {}\mRightarrow{}  (\muparrow{}same-binding(map(F;bnds);bnds;F  v;v)))\mkleeneclose{};
  \mkleeneopen{}bnds\mkleeneclose{}]\mcdot{}
  THEN  Try  (Trivial)
  )

---

Home Index