proposition: Lemma Variant_termination (Var : WfVariant ) : terminates .
proof: Proof. intro x; apply Acc_incl with (fun a b => m a < m b). - intros a b H; now apply decr. - apply Acc_inverse_image, wf. Qed.
imports: Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)