proposition: Lemma acc_from_power_af (p : WFT X) (T R : X → X → Prop) y k : (∀ x z, clos_refl_trans _ T z y -> clos_trans_1n X (power k T) x z ∧ R z x → False) → SecureBy R (secure_power k p) → Acc T y.
proof: Proof. induction p as [|p IHp] in T, R, y, k |- * . Admitted. Lemma wf_from_power_af (p : WFT X) (T R : X → X → Prop) k : (∀ x y, clos_trans_1n X (power k T) x y ∧ R y x → False) → SecureBy R p → well_founded T. Proof. intros. intro x. eapply acc_from_power_af; eauto. apply secure_by_power. apply H0. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)