proposition: Lemma acc_power (T : X -> X -> Prop) x k : Acc T x -> Acc (power k T) x.
proof: Proof. intros. apply Acc_clos_trans in H. revert H. apply acc_incl. intros. now apply (power_clos_trans _ k). Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)