proposition: Lemma wf_from_af (p : WFT X) (T R : X → X → Prop) : (∀ x y, clos_trans_1n X T x y ∧ R y x → False) → SecureBy R p → well_founded T.
proof: Proof. intros. intro x. eapply acc_from_af;eauto. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)