proposition: Fact in_nat_sorted_1 x : nat_sorted (x::nil).
proof: Proof. intros [ | ? [] ] ? [] ? ? ?; discriminate. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)