{α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {decls : Array (Std.Sat.AIG.Decl α)} →
        {idx : ℕ} →
          (max : ℕ) →
            (map : Std.HashMap α ℕ) →
              Std.Sat.AIG.RelabelNat.State.Inv1 max map →
                Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map → Std.Sat.AIG.RelabelNat.State α decls idx