proposition: Theorem list_bool_succ_rect : forall l, P l.
proof: Proof. Proof using HP0 HPS. intro; apply list_bool_succ_rec with (1 := eq_refl). Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)