blob: 5fb4839847281067fcd74ebd11a3e4bf8b02670a (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Setoid Coq.Program.Basics.
Global Open Scope program_scope.
Axiom foo : forall A (f : A -> A), f ∘ f = f.
Require Import Coq.Program.Combinators.
Hint Rewrite foo.
Theorem t {A B C D} (f : A -> A) (g : B -> C) (h : C -> D)
: f ∘ f = f.
Proof.
rewrite_strat topdown (hints core).
|
