proposition: Lemma lem_lelst_perm_rev {A} {dto : DecTotalOrder A} : forall l1 l2 x, Permutation l1 l2 -> LeLst x l2 -> LeLst x l1.
proof: Proof. induction 1; sauto. Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Sorting.Permutation Program