## Stream: new members

### Topic: Equality of inductive type variants

#### Spencer Killen (May 28 2020 at 17:36):

Given

inductive Choices
| A
| B
open Choices


is it possible to prove

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


Without introducing new axioms?

#### Spencer Killen (May 28 2020 at 17:37):

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 (May 28 2020 at 17:38):

Choices.no_confusion

#### Pedro Minicz (May 28 2020 at 23:04):

Reid Barton said:

Aptly named.

Last updated: May 08 2021 at 03:17 UTC