Как я могу остановить метод simp от разделения кортежа на его компоненты?
Пример. Если я напишу
fun foo where "foo z = blah z"
lemma "∃z :: nat × nat × nat × nat × nat. foo z"
состояние доказательства - ∃z. foo z. Если я тогда напишу
apply (simp)
состояние доказательства становится ∃a aa ab ac b. blah (a, aa, ab, ac, b). Мне нравится, что simp расширил foo на blah, но я бы предпочел оставить мою переменную z как есть.
