Commit 49a03d40 authored by Ralf Jung's avatar Ralf Jung

solve_proper_unfold: support functions with more arguments

parent 29a0e002
......@@ -326,6 +326,8 @@ we proceed by repeatedly using [f_equiv]. *)
Ltac solve_proper_unfold :=
(* Try unfolding the head symbol, which is the one we are proving a new property about *)
lazymatch goal with
| |- ?R (?f _ _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
......
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