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.
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.