test-suite/output/NoAxiomFromR.v


1
2
3
4
5
6
7
8
9
10

Require Import Psatz.

Inductive TT : Set :=
| C : nat -> TT.

Lemma lem4 : forall (n m : nat),
S m <= m -> C (S m) <> C n -> False.
Proof. firstorder lia. Qed.

Print Assumptions lem4.