proposition: Fact list_bool_valid_dec k lb : { ln | list_bool_valid k lb ln } + { ln | list_bool_invalid k lb ln }.
proof: Proof. destruct (list_bool_decomp k lb) as [ (ln & lc & H1 & H2) | (ln & [|p] & H1 & H2) ]. * right; exists ln, lc; tauto. * left; exists ln; split; auto; subst; solve list eq. * right; exists ln, (list_repeat Zero (S p)); split; auto. right; split; auto; exists p; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)