* are_convertible bug solved, arguments of application where
compared allowing cumulativity. This allowed to prove Type0=Type1.
* cases tactic speedup in the simplest case of an inductive type
* are_convertible bug solved, arguments of application where
compared allowing cumulativity. This allowed to prove Type0=Type1.
* cases tactic speedup in the simplest case of an inductive type