proposition: Fact lc_nil_inv_r l : l ⪼ nil -> l = nil.
proof: Proof. intros H; apply lc_lequiv in H as []; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)