Hi all, How can I tell the auto-method NOT to do pair splitting automatically? E.g. having consts P::"'a*'a => bool" lemma test: "!!a. P a \<and> (True --> True)" apply auto gives "!!a b. P (a,b)" but I need: !!a. P a regards and thanks in advance, Peterp.s. I could have used simp for this particular example, but for my actual task, I need auto.