Problem with induction hypothesis/generalization

Stream: new members

[Marcus Rossel]

Ok, I've got another one which is a bit more complicated:

inductive E
structure D where es : Nat → E
inductive C
structure B where cs : Nat → List C
structure A where bs : Nat → B

def CEquivE : C → E → Prop := sorry

def makeE {a : A} {b : B} (hb : ∃ i, a.bs i = b) {c : C} {i} (hc : c ∈ b.cs i) : E := sorry

example (a : A) (b : B) (hb : ∃ i, a.bs i = b) (i : Nat) :
  List.forall₂ CEquivE (b.cs i) ((b.cs i).attach.map (makeE hb ·.property)) := by
  generalize b.cs i = x

Here I can't generalize, because tactic 'generalize' failed, result is not type correct.
Simply trying induction b.cs i has the same problem.

I'm guessing it has something to do with the fact that I'm using attach on b.cs i, but I don't know how to resolve the issue.