new codegen: tests/lean/run/discrRefinement2.lean fails

[zwarich]

The items

def ex2 {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
  match h, m with
  | HEq.refl _, m => m

def ex3 {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
  match h₁, h₂ with
  | HEq.refl _, h₂ => h₂

cause the errors

tests/lean/run/discrRefinement2.lean:6:4: error: unsupported `HEq.casesOn` application during code generation
tests/lean/run/discrRefinement2.lean:10:4: error: unsupported `HEq.casesOn` application during code generation

[leodemoura]

Fixed by #6311