---

Step * of Lemma alpha-avoid_wf

No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[L:varname() List].  alpha-avoid(L;t) ∈ term(opr) supposing ¬(nullvar() ∈ L)
BY
{ ProveWfLemma }

1
1. opr : Type
2. t : term(opr)
3. L : varname() List
4. ¬(nullvar() ∈ L)
5. x : {v:varname()| (v ∈ all-vars(t))} 
6. (alist-map(VarDeq;alpha-rename-alist(t;L)) x) = nullvar() ∈ varname()
⊢ x = nullvar() ∈ varname()

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:term(opr)].  \mforall{}[L:varname()  List].
    alpha-avoid(L;t)  \mmember{}  term(opr)  supposing  \mneg{}(nullvar()  \mmember{}  L)


By

---

Latex:
ProveWfLemma

---

Home Index