{P : Sort u} →
  {α β : Type} →
    {inst : BEq α} →
      {inst_1 : Hashable α} →
        {t : Lean.Compiler.LCNF.CacheExtension α β} →
          {α' β' : Type} →
            {inst' : BEq α'} →
              {inst'_1 : Hashable α'} →
                {t' : Lean.Compiler.LCNF.CacheExtension α' β'} →
                  α = α' →
                    β = β' →
                      inst ≍ inst' →
                        inst_1 ≍ inst'_1 → t ≍ t' → Lean.Compiler.LCNF.CacheExtension.noConfusionType P t t'