---

Step * of Lemma free-vars-all-vars

No Annotations
∀[opr:Type]. ∀t:term(opr). ∀x:varname().  ((x ∈ free-vars(t)) ⇒ (x ∈ all-vars(t)))
BY
{ (Intro THEN BLemma `term-induction` THEN Auto THEN Try (((Assert varterm(v) ∈ term(opr) BY Auto) THEN Auto))) }

1
1. [opr] : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr). ((bt ∈ bts) ⇒ (∀x:varname(). ((x ∈ free-vars(snd(bt))) ⇒ (x ∈ all-vars(snd(bt))))))
4. f : opr
5. x : varname()
6. (x ∈ free-vars(mkterm(f;bts)))
⊢ (x ∈ all-vars(mkterm(f;bts)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}t:term(opr).  \mforall{}x:varname().    ((x  \mmember{}  free-vars(t))  {}\mRightarrow{}  (x  \mmember{}  all-vars(t)))


By

---

Latex:
(Intro
  THEN  BLemma  `term-induction`
  THEN  Auto
  THEN  Try  (((Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  THEN  Auto)))

---

Home Index