Unification error during inductive type verification in presence of AC operators

[bodeveix]

The declaration of an inductive type generates an unification proof obligation which cannot be solved in presence of an AC operator:

symbol Prop : TYPE;
injective symbol π: Prop → TYPE;
builtin "Prop" ≔ Prop;
builtin "P" ≔ π;

symbol context: TYPE;
symbol □ : context;
associative commutative symbol ∙ : context → context → context;
notation ∙ infix right 1;

symbol γ: context → context;
rule □ ∙  $H ↪ $H;

// OK
inductive valid1: context → TYPE ≔
| R1 H1 H2 : valid1 (H1 ∙ H2) → valid1 H2;

// BUG
inductive valid2: context → TYPE ≔
| R2 H1 H2 : valid2 (H1 ∙ H2) → valid2 H1;

// BUG
inductive valid3: context → TYPE ≔
| R3 P H : valid3 (H ∙ γ P) → valid3 H;

// BUG
inductive valid4: context → TYPE ≔
| R4 P H : valid4 (γ P ∙ H) → valid4 H;