proposition: Fact lc_lhd l m : l ⪼ m -> lhd m -> lhd l.
proof: Proof. induction 1 as [ | x l m H IH | | | ]; eauto. rewrite !lhd_cons_iff; intros []; auto. 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)