Hello,

I am trying to define a datatype for intervals of natural numbers: either a “proper” interval or the empty interval: something like

```
Inductive t :=
| Range: forall d1 d2, d1 <= d2 -> t
| Empty: t.
```

Then I define the “merge” function (the smallest interval containing two intervals) by:

```
Definition merge (a1 a2 : t) :=
match a1, a2 with
| Empty, _ -> a2
| _, Empty -> a1
| Range l1 r1 H1, Range l2 r2 H2 -> Range (min l1 l2) (max r1 r2) _
end
```

and the `In`

predicate:

```
Definition In (d : nat) (a : t) : Prop :=
match a with
| Empty => False
| Range l r _ => l <= d /\ d <= r
end.
```

However the fact that the proof of the inequality is carried around makes Leibniz equality for `t`

pretty much useless. Is there a way to make the proof in the `Range`

constructor somehow irrelevant so that Leibniz equality can be used (ideally without assuming any extra axioms)? Or maybe there a reformulation of the definition without this problem?

Otherwise, how “bad” would it be if I were to add the following axiom to my development:

```
Axiom t_eq: forall l r H1 H2, Range l r H1 = Range l r H2.
```

?

Thanks! All suggestions welcome!

Best wishes,

Nicolás