proposition: Lemma wf_from_wqo : forall (X:Type) (p : WFT X) (R : X -> X -> Prop), transitive X R -> SecureBy R p -> well_founded (fun x y => R x y /\ ~ R y x).
proof: Proof. intros. apply wf_from_af with (R := R) (p := p). intros. destruct H1. assert (~ R y x). induction H1. destruct H1. apply H3. unfold not in *. intros. apply IHclos_trans_1n. destruct H1. apply (H _ _ _ H4 H1). destruct H1. apply (H _ _ _ H4 H1). unfold not in H3. apply H3. apply H2. apply H0. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)