Closed strub closed 1 month ago
op p : int -> bool. lemma foo x : p x. proof. pose S (x : int) := x. rewrite -/(S x). pose G x := S x. rewrite -/(G x). rewrite /G.