test-suite/micromega/bug_12791.v


1
2
3
4
5
6
7
8
9

Require Import Lia.

Definition t := nat.

Goal forall (a b: t), let c := a in b = a -> b = c.
Proof.
  intros a b c H.
  lia.
Qed.