proposition: Fact list_bool_succ_nil l : list_bool_succ nil l -> l = Zero::nil.
proof: Proof. intros H; symmetry; revert H; apply list_bool_succ_fun. constructor 2 with (k := 0). Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)