Induct_on / using example

[mn200]

Induct_on `RTC` using relationTheory.RTC_ALT_RIGHT_INDUCT

should work.

[konrad-slind]

How is this different/better than HO_MATCH_MP_TAC relationTheory.RTC_ALT_RIGHT_INDUCT? Is there some kind of normalization/search for an expression in the goal with RTC as its operator?

…

On Wed, Nov 16, 2022 at 7:38 PM Michael Norrish ***@***.***> wrote: Induct_on `RTC` using relationTheory.RTC_ALT_RIGHT_INDUCT should work. — Reply to this email directly, view it on GitHub <#1073>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAIOAD4LHU2DHAM2CA4CLCTWIWEDBANCNFSM6AAAAAASC3FWM4> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[mn200]

Yes, exactly.

Induct_on `RTC`

does this already (using the default principle) but the form of the alt-right theorem defeats this machinery.