Equality of inductive type variants

Stream: new members

[Spencer Killen]

Given

inductive Choices
| A
| B
open Choices

is it possible to prove

example (h : A = B) : false := sorry

Without introducing new axioms?

[Spencer Killen]

Nothing opposed to adding the axioms if I need them, I just don't want to if I don't need to and there's something I'm not understanding about inductive types

[Johan Commelin]

Choices.no_confusion

[Reid Barton]

Also see https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

[Pedro Minicz]

Reid Barton said:

Also see https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

Aptly named.