proposition: Lemma acc_from_af: forall (X:Type) (p : WFT X) (R : X -> X -> Prop) (T : X -> X -> Prop) y, (forall x z, clos_refl_trans X T z y -> clos_trans_1n X T x z /\ R z x -> False) -> SecureBy R p -> Acc T y.
proof: Proof. intros X p. induction p. intros. simpl in H0. apply Acc_intro. intros. edestruct (H y0 y). apply rt_refl. split. constructor 1. apply H1. apply H0. intros. apply Acc_intro. intros z HT. simpl in H1. remember (H1 y). eapply H with (R := fun y0 z => R y0 z \/ R y y0). 2: apply s. intros. simpl in H2. simpl in H3. destruct H3. destruct H4. eapply H0. eapply trans_clos_left. apply HT. apply H2. split. apply H3. apply H4. eapply H0. eapply trans_clos_left. apply HT. apply H2. split. apply H3. destruct (H0 z0 y). apply rt_refl. split. 2: apply H4. eapply trans_clos_left_aux. apply HT. apply H2. Defined.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)