blob: a89f9ac30796f48aa096e8e9fceb0e0a80b4ea30 (
plain)
1
2
3
4
5
6
7
8
9
10
|
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).
Abort.
|
