---

Step * of Lemma alpha-aux-refl

No Annotations
∀[opr:Type]. ∀a:term(opr). ∀vs:varname() List.  alpha-aux(opr;vs;vs;a;a)
BY
{ (Intro
   THEN ((BLemma `term-induction` THENW Auto)
         THEN Intro
         THEN (((Assert varterm(v) ∈ term(opr) BY Auto) THEN RenameVar `a' (-2)) ORELSE RepeatFor 2 (Intro)))
   THEN Intro
   THEN ((RWO "alpha-aux-mkterm" 0 THEN Auto)
   ORELSE (Unfold `alpha-aux` 0 THEN Reduce 0 THEN RWO "same-binding-refl" 0 THEN Auto)
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}a:term(opr).  \mforall{}vs:varname()  List.    alpha-aux(opr;vs;vs;a;a)


By

---

Latex:
(Intro
  THEN  ((BLemma  `term-induction`  THENW  Auto)
              THEN  Intro
              THEN  (((Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  THEN  RenameVar  `a'  (-2))
              ORELSE  RepeatFor  2  (Intro)
              ))
  THEN  Intro
  THEN  ((RWO  "alpha-aux-mkterm"  0  THEN  Auto)
  ORELSE  (Unfold  `alpha-aux`  0  THEN  Reduce  0  THEN  RWO  "same-binding-refl"  0  THEN  Auto)
  ))

---

Home Index