destruct (PeanoNat.Nat.eqb_spec x1 x2) as [->|Dx1x2].

Want to apply it on another data type

```
Definition mass (m1 m2: mas) : bool :=
match m1, m2 with
| lit, lit => true
| med, med => true
| larg, larg => true
| _, _ => false
end.
```

But it not does not replace m1 with m2. Therefore i am unable to simplify it further.

you should prove the equivalent of `eq_spec`

```
Definition mass (m1 m2: mas) : bool :=
match m1, m2 with
| lit, lit => true
| med, med => true
| larg, larg => true
| _, _ => false
end.
Lemma mas_spec x y : reflect (x = y) (mass x y).
Proof.
destruct x; destruct y; simpl; constructor; auto; try discriminate.
Qed.
Goal forall (P: mas -> Prop) x y, P x -> P y.
Proof.
intros P x y.
destruct (mas_spec x y) as [-> | xDy].
```

Thank u.

Last updated: Oct 04 2023 at 21:01 UTC