proposition: Fact list_One_inj a b : list_repeat One a = list_repeat One b -> a = b.
proof: Proof. intros H; apply f_equal with (f := @length _) in H; revert H. do 2 rewrite list_repeat_length; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)