{α : Type} →
  {inst : Hashable α} →
    {inst_1 : DecidableEq α} →
      {old : Std.Sat.AIG α} →
        {P : Sort u} →
          {aig : Std.Sat.AIG α} →
            {out cout : aig.Ref} →
              {hle : old.decls.size ≤ aig.decls.size} →
                {aig' : Std.Sat.AIG α} →
                  {out' cout' : aig'.Ref} →
                    {hle' : old.decls.size ≤ aig'.decls.size} →
                      { aig := aig, out := out, cout := cout, hle := hle } =
                          { aig := aig', out := out', cout := cout', hle := hle' } →
                        (aig ≍ aig' → out ≍ out' → cout ≍ cout' → P) → P