binder_induction avoiding an immediate argument of the inductive predicate fails

[dtraytel]

lemma EFVrs_EsubI1:
  assumes
    "z ∈ EFVrs e"
    "|supp (δ :: 'a ⇒ 'a::var)| <o |UNIV :: 'a set|"
    "|SSupp (Ector ∘ η) ρ| <o |UNIV :: 'a set|"
    "|SSupp (Ector ∘ η') ρ'| <o |UNIV :: 'a set|"
  shows "δ z ∈ EFVrs (Esub δ ρ ρ' e)"
  using assms(1,5) unfolding EFVrs_def mem_Collect_eq
  apply (binder_induction z e arbitrary: a avoiding: "imsupp δ" "IImsupp' (Ector o η) EVrs ρ" "IImsupp' (Ector o η') EVrs ρ'" "EVrs e" rule: Efreee.strong_induct)

fails in a context where EVrs is axiomatized (not registered in an MRBNF).

Working workaround:

lemma EFVrs_EsubI1:
  assumes
    "z ∈ EFVrs e"
    "|supp (δ :: 'a ⇒ 'a::var)| <o |UNIV :: 'a set|"
    "|SSupp (Ector ∘ η) ρ| <o |UNIV :: 'a set|"
    "|SSupp (Ector ∘ η') ρ'| <o |UNIV :: 'a set|"
     "a = e"
  shows "δ z ∈ EFVrs (Esub δ ρ ρ' e)"
  using assms(1,5) unfolding EFVrs_def mem_Collect_eq
  apply (binder_induction z e arbitrary: a avoiding: "imsupp δ" "IImsupp' (Ector o η) EVrs ρ" "IImsupp' (Ector o η') EVrs ρ'" "EVrs a" rule: Efreee.strong_induct)