Rewrite.agda:13,1-36 Cannot rewrite by equation of type x ≈ y when checking that the clause thm P x y px rewrite lem x y = ? has type {A : Set} (P : A → Set) (x y : A) → P x → P y