destruct/case transformations incorrectly handle polymorphic formulas
destruct don't take into account the fact that the formula they are applied to can be implicitely quantified over a type variable.
This allows us to prove
false in the following ways :
case (forall x y : 'a. x = y)and pass the resulting tasks to Eprover
first prove that
(forall x y : 'a. x = y) \/ (not forall x y : 'a. x = y)(by calling CVC4 for example), apply
destructto this hypothesis and pass the resulting tasks to Eprover
What's happening ?
forall x y : 'a. x = y should be understood as
forall 'a. forall x y : 'a. x = y. When we apply
case on this formula, the negation incorrectly goes under the type quantification in the second task.