See also Conv.RENAME_VARS_CONV
On Fri, Aug 3, 2018 at 9:00 AM Chun Tian (binghe)
wrote:
> Hi Thomas,
>
> thanks very much, now I see the possibility of changing whatever variable
> names I want! (I never knew nor needed ALPHA before, although
> alpha-conversion is familiar to me)
>
> —Chun
>
>
Hi Thomas,
thanks very much, now I see the possibility of changing whatever variable names
I want! (I never knew nor needed ALPHA before, although alpha-conversion is
familiar to me)
—Chun
> Il giorno 03 ago 2018, alle ore 15:03, Thomas Tuerk
> ha scritto:
>
> Hi Chun,
>
> the easiest
Hi Chun,
the easiest way is using alpha-equivalence. If you really just want to
rename vars, you can state the new form explicitly and use
apha-equivalence via e.g. ALPHA directly. Tools like METIS_TAC should in
theory be able to do it, but in practice try to do too much and
therefore time out, I
Hi,
suppose I have proved (or generated) a theorem like this:
⊢ ∀a0 a1.
a0 ∼ a1 ⇔
∀u.
(∀E1. a0 --u-> E1 ⇒ ∃E2. a1 --u-> E2 ∧ E1 ∼ E2) ∧
∀E2. a1 --u-> E2 ⇒ ∃E1. a0 --u-> E1 ∧ E1 ∼ E2
but I don’t like the variables names (a0, a1, E1, E2), I want a new
