blob: e71ddaf71f0e263409cd261a03999d96d93b08db (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Inductive True : Prop := I.
Class Lift (T : Type).
Axiom closed_increment : forall {T} {H : Lift T}, True.
Create HintDb core.
Lemma closed_monotonic T (H : Lift T) : True.
Proof.
Set Printing Universes.
auto using closed_increment. Show Universes.
Qed.
(* also fails with -nois, so the content of the hint database does not matter
*)
|
