Generated elimination principle is missing some induction hypotheses

[RalfJung]

Given this code:

From Coq Require Export Lia.
From Equations Require Export Equations.

Definition var := nat.

Inductive type : Type :=
  | Nat : type
  (* De Bruijn encoding *)
  | TForall : type -> type
  | TExists : type -> type
.

Inductive expr :=
  | Lit (n : nat)
  (* Polymorphism *)
  | TApp (e : expr)
  | TLam (e : expr)
  | Pack (e : expr)
  | Unpack (e1 : expr) (e2 : expr)
.

Inductive val :=
  | LitV (n : nat)
  | TLamV (e : expr)
  | PackV (v : val)
.

Definition big_step : expr -> val -> Prop.
Proof. Admitted.

Inductive val_or_expr : Type :=
| inj_val : val -> val_or_expr
| inj_expr : expr -> val_or_expr.

Equations type_size (A : type) : nat :=
  type_size Nat := 1;
  type_size (TForall A) := type_size A + 2;
  type_size (TExists A) := type_size A + 2;
.

Equations type_interp_measure (ve : val_or_expr) (A : type) : nat :=
  type_interp_measure (inj_expr e) A := 1 + type_size A;
  type_interp_measure (inj_val v) A := type_size A.

Definition sem_type := val -> Prop.
Definition tyvar_interp := var -> sem_type.

Definition scons : sem_type -> tyvar_interp -> tyvar_interp.
Proof. Admitted.

Equations type_interp (ve : val_or_expr) (A : type) (delta : tyvar_interp) : Prop by wf (type_interp_measure ve A) := {
  type_interp (inj_val v) Nat delta =>
    exists n, v = LitV n ;
  (** forall case *)
  type_interp (inj_val v) (TForall A) delta =>
    exists e, v = TLamV e /\
      forall tau : sem_type, type_interp (inj_expr e) A (scons tau delta);
  (** exists case *)
  type_interp (inj_val v) (TExists A) delta =>
    exists v', v = PackV v' /\
      exists tau : sem_type, type_interp (inj_val v') A (scons tau delta);

  (** expression relation *)
  type_interp (inj_expr e) A delta =>
    exists v, big_step e v /\ type_interp (inj_val v) A delta
}.
Next Obligation. repeat simp type_interp_measure; simp type_size; lia. Qed.
Next Obligation. repeat simp type_interp_measure; simp type_size; lia. Qed.

I would expect the generated type_interp_elim to be strong enough to do recursive reasoning about this function. However, that is not the case:

type_interp_elim :
forall P : val_or_expr -> type -> tyvar_interp -> Prop -> Type,
(forall (v : val) (delta : tyvar_interp), P (inj_val v) Nat delta (exists n : nat, v = LitV n)) ->
(forall (v : val) (A : type) (delta : tyvar_interp),
 P (inj_val v) (TForall A) delta
   (exists e : expr,
      v = TLamV e /\ (forall tau : sem_type, type_interp (inj_expr e) A (scons tau delta)))) ->
(forall (v : val) (A : type) (delta : tyvar_interp),
 (forall (v' : val) (tau : sem_type),
  P (inj_val v') A (scons tau delta) (type_interp (inj_val v') A (scons tau delta))) ->
 P (inj_val v) (TExists A) delta
   (exists v' : val,
      v = PackV v' /\ (exists tau : sem_type, type_interp (inj_val v') A (scons tau delta)))) ->
(forall (e : expr) (A : type) (delta : tyvar_interp),
 (forall v : val, P (inj_val v) A delta (type_interp (inj_val v) A delta)) ->
 P (inj_expr e) A delta (exists v : val, big_step e v /\ type_interp (inj_val v) A delta)) ->
forall (ve : val_or_expr) (A : type) (delta : tyvar_interp), P ve A delta (type_interp ve A delta)

Notice, in particular, the TForall case:

(forall (v : val) (A : type) (delta : tyvar_interp),
 P (inj_val v) (TForall A) delta
   (exists e : expr,
      v = TLamV e /\ (forall tau : sem_type, type_interp (inj_expr e) A (scons tau delta)))) ->

This asks me to prove that case without any inductive hypothesis. That will usually not be provable, so I need to do manual size induction on the measure instead.

I tried simplifying the example by removing the delta; then the bug disappears.

Would be great to get a usable induction principle directly from Equations. :)