{P : Sort u} →
  {α : Type} →
    {inst : Hashable α} →
      {inst_1 : DecidableEq α} →
        {aig : Std.Sat.AIG α} →
          {w : ℕ} →
            {t : aig.RefVec w} →
              {α' : Type} →
                {inst' : Hashable α'} →
                  {inst'_1 : DecidableEq α'} →
                    {aig' : Std.Sat.AIG α'} →
                      {w' : ℕ} →
                        {t' : aig'.RefVec w'} →
                          α = α' →
                            inst ≍ inst' →
                              inst_1 ≍ inst'_1 →
                                aig ≍ aig' → w = w' → t ≍ t' → Std.Sat.AIG.RefVec.noConfusionType P t t'