---

Step * of Lemma alpha-rename-alist_wf

No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[L:varname() List].  (alpha-rename-alist(t;L) ∈ (varname() × varname()) List)
BY
{ ((Intros THEN Unhide)
   THEN Unfold `alpha-rename-alist` 0
   THEN GenConclAtAddrType ⌜varname() List × ((varname() × varname()) List)⌝ [2;1]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:term(opr)].  \mforall{}[L:varname()  List].
    (alpha-rename-alist(t;L)  \mmember{}  (varname()  \mtimes{}  varname())  List)


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  Unfold  `alpha-rename-alist`  0
  THEN  GenConclAtAddrType  \mkleeneopen{}varname()  List  \mtimes{}  ((varname()  \mtimes{}  varname())  List)\mkleeneclose{}  [2;1]\mcdot{}
  THEN  Auto)

---

Home Index