Eliminating on decidable equality

Stream: new members

[Oskar Berndal]

Hi! I'm trying to define a Syntax (with dB indices). As part of that I want to define substitution. This however requires me to eliminate on whether two variables (integers) are equal. I tried to define a Term of Syntax by doing

cases (decidable.em (x = major)),

where x and major are nats in the context. But it says that 'induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop. I want to ask, how can I eliminate on the decidability of equality of nats such that I can define a term of any type? Thanks! =)

[Johan Commelin]

@Oskar Berndal Do you just want

if x = major then foo else bar

[Oskar Berndal]

Oh yes I believe I do. Thanks! =)

[Mario Carneiro]

you can also use by_cases x = major in tactic mode