---

Step * of Lemma free-vars_functionality

No Annotations
∀[opr:Type]. ∀t1,t2:term(opr).  (alpha-eq-terms(opr;t1;t2) ⇒ (free-vars(t1) = free-vars(t2) ∈ (varname() List)))
BY
{ (Intro
   THEN (Enough to prove ∀t1,t2:term(opr). ∀bnds1,bnds2:varname() List.
                           (alpha-aux(opr;bnds1;bnds2;t1;t2)
                           ⇒ (free-vars-aux(bnds1;t1) = free-vars-aux(bnds2;t2) ∈ (varname() List)))
          Because (RepeatFor 2 (ParallelLast)
                   THEN RepeatFor 2 ((D -1 With ⌜[]⌝  THENA Auto))
                   THEN Fold `free-vars` (-1)
                   THEN Fold `alpha-eq-terms` (-1)
                   THEN Trivial))
   ) }

1
1. [opr] : Type
⊢ ∀t1,t2:term(opr). ∀bnds1,bnds2:varname() List.
    (alpha-aux(opr;bnds1;bnds2;t1;t2) ⇒ (free-vars-aux(bnds1;t1) = free-vars-aux(bnds2;t2) ∈ (varname() List)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}t1,t2:term(opr).    (alpha-eq-terms(opr;t1;t2)  {}\mRightarrow{}  (free-vars(t1)  =  free-vars(t2)))


By

---

Latex:
(Intro
  THEN  (Enough  to  prove  \mforall{}t1,t2:term(opr).  \mforall{}bnds1,bnds2:varname()  List.
                                                  (alpha-aux(opr;bnds1;bnds2;t1;t2)
                                                  {}\mRightarrow{}  (free-vars-aux(bnds1;t1)  =  free-vars-aux(bnds2;t2)))
                Because  (RepeatFor  2  (ParallelLast)
                                  THEN  RepeatFor  2  ((D  -1  With  \mkleeneopen{}[]\mkleeneclose{}    THENA  Auto))
                                  THEN  Fold  `free-vars`  (-1)
                                  THEN  Fold  `alpha-eq-terms`  (-1)
                                  THEN  Trivial))
  )

---

Home Index