Subtyping heuristic and auto case

[craff]

Currently, we use in subtyping a heuristic testing is the term (int t : A < B) is a value.
This heuristic seems in fact to test if we already unrolled fixpoint ... And is
not so clear.

As a side effect, this heuristic forces subtyping of sums to use introduce a term
Preventing to replace the current term in a case anlysis with only one case with
a witness.

But this term with one case produce useless computation in the pool and useless
case analysis in auto_prove.