Теория с двумя сильно конструктивизируемыми моделями

Строится пример полной, допускающей элиминацию кванторов теории, имеющей точно две сильно конструктивизируемые модели, причем обе они автоустойчивы относительно всех конструктивизаций.