Stuck.agda:12,1-10 I'm not sure if there should be a case for the constructor e, because I get stuck when trying to solve the following unification problems (inferred index ≟ expected index): j ≟ i j ≟ x when checking the definition of f