{P : Sort u} →
  {candidates candidates' : Std.HashMap Lean.FVarId Lean.Compiler.LCNF.JoinPointFinder.CandidateInfo} →
    { candidates := candidates } = { candidates := candidates' } → (candidates = candidates' → P) → P