proposition: Fact lc_nil_inv_l l : nil ⪼ l -> l = nil.
proof: Proof. intros H; apply lc_length in H. destruct l; simpl in *; auto; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)