Commit 29a0e002 authored by Ralf Jung's avatar Ralf Jung

f_equiv: recognize 2-level pointwise_relation

parent cae9ec0f
......@@ -316,6 +316,7 @@ Ltac f_equiv :=
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
| H : pointwise_relation _ (pointwise_relation _ ?R) ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => simple apply H
end;
try simple apply reflexivity.
Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment