proposition: Lemma acc_from_af (p : WFT X) (T R : X → X → Prop) y : (∀ 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. induction p as [|p IHp] in T, R, y |- * . + simpl. intros. constructor. intros z Tz. specialize (H z y). elim H. constructor 2. split; auto. constructor. auto. + intros cond secure. constructor. intros z Tzy. simpl in secure. specialize (IHp y T (fun y0 z0 => R y0 z0 \/ R y y0) z). apply IHp; auto. intros x w wz. assert(wy: clos_refl_trans X T w y). { econstructor 3. eauto. now constructor. } pose proof (cond x w wy). intuition. specialize (cond w y). apply cond. constructor 2. intuition. apply clos_trans_n1_1n. eapply clos_refl_trans_right; eauto. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)