blob: 6a2f9672d3508928f9f1bb5fd9ab87f9c14ac43d (
plain)
1
2
3
4
5
6
7
8
9
10
|
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.
auto using closed_increment. Show Universes.
Qed.
(* also fails with -nois, so the content of the hint database does not matter
*)
|
