destruct/case transformations incorrectly handle polymorphic formulas
The transformations case
and 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 :

apply
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), applydestruct
to this hypothesis and pass the resulting tasks to Eprover
What's happening ?
The formula 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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information