∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {n : ℕ} {check persistent : Bool}
  {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11} {fvarId_1 : Lean.FVarId}
  {n_1 : ℕ} {check_1 persistent_1 : Bool} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11},
  Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h =
      Lean.Compiler.LCNF.Code.inc fvarId_1 n_1 check_1 persistent_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ k = k_1