proposition: Lemma wf_from_af : forall (X:Type) (p : WFT X) (R : X -> X -> Prop) (T : X -> X -> Prop), (forall x y, clos_trans_1n X T x y /\ R y x -> False) -> SecureBy R p -> well_founded T.
proof: Proof. intros. unfold well_founded. intro y. eapply acc_from_af. 2: apply H0. intros. eapply H. apply H2. Defined.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)