Anomaly "splitting Equations missing constraints in (anonymous)"

[henriquebg99]

trafficstars

Given the inductive

Inductive eq' : forall (A: Type), A -> A -> Prop :=
  | eq_refl' : forall (A: Type) (a: A), eq' A a a                                  
  | eq_funext' : forall (A B: Type) (f g: A -> B), (forall x, eq' B (f x) (g x)) -> eq' (A -> B) f g.

The following equations raise an error.

Equations eq_sym' {A: Type} {a b : A} (e: eq' A a b) : eq' A b a :=
    eq_sym' (eq_refl' A a) := eq_refl' A a ;
    eq_sym' (eq_funext' A B f g H) := eq_funext' A B g f (fun x => eq_sym' (H x)).

The error is: Anomaly "splitting Equations missing constraints in (anonymous)"