proposition: Fact list_bool_succ_neq : forall l m, list_bool_succ l m -> l <> m.
proof: Proof. intros ? ? [ [|k] l | [|k] ]; discriminate. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)