proposition: Lemma acc_from_af: forall (X:Type) (R : X -> X -> Prop), almost_full R -> forall (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) -> Acc T y.
proof: Proof. intros X R afPred. induction afPred. intros. apply Acc_intro. intros. edestruct H0. constructor 2. split. constructor 1. apply H1. apply H. intros. apply Acc_intro. intros z HT. remember (H y). eapply H0. intros. intros. destruct H3. destruct H4. eapply H1. eapply trans_clos_left. apply HT. apply H2. split. apply H3. apply H4. eapply H1. apply rt_refl. split. 2: apply H4. eapply trans_clos_left_aux. apply HT. apply H2. Defined.
imports: Coq(Arith Relations)