proposition: Lemma Hvariant_Termination {A : Type} {lt : relation A} (Hwf : well_founded lt) (m : Hydra -> A) : @Hvariant _ _ Hwf free m -> Termination.
proof: Proof. destruct 1. intro x; apply Acc_incl with (fun h' h => lt (m h') (m h)). - intros h' h H; destruct H; apply variant_decr with x0. + intro ; subst h; apply (head_no_round_n _ _ H). + exists x0; easy. - apply Acc_inverse_image, Hwf. Qed.
imports: Coq(Arith Lia List Relation_Operators Operators_Properties Peano_dec Wellfounded.Inverse_Image Wellfounded.Inclusion) hydras(More_Arith Epsilon0 Hessenberg Simple_LexProd MoreLibHyps)