test-suite/micromega/bug_11089.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Require Import Lia.
Unset Lia Cache.
Definition t := nat.
Goal forall (n : t), n = n.
Proof.
  intros.
  lia.
Qed.
Goal let t' := nat in forall (n : t'), n = n.
Proof.
  intros.
  lia.
Qed.