{P : Sort u} →
  {vs vs' : List Lean.Compiler.LCNF.UnreachableBranches.Value} →
    Lean.Compiler.LCNF.UnreachableBranches.Value.choice vs = Lean.Compiler.LCNF.UnreachableBranches.Value.choice vs' →
      (vs = vs' → P) → P