proposition: Lemma secure_from_wf : forall (X:Type) (R : X -> X -> Prop) (wfR : well_founded R) (decR : dec_rel R), SecureBy (fun x y => ~ R y x) (SUP (af_tree wfR decR)).
proof: Proof. intros. rewrite sup_rewrite. unfold af_tree. intro x. remember (wfR x) as xAcc. clear HeqxAcc. apply (@well_founded_induction X R wfR (fun (x:X) => forall (xAcc : Acc R x), SecureBy (fun y z => ~ R z y \/ ~ R y x) (af_tree_iter decR xAcc))). intros y H. intro xAccy. destruct xAccy. simpl. intro z. destruct (decR y z). simpl. right. right. apply n. eapply sec_strengthen. 2: { apply H. apply r. } intros. simpl in H0. destruct H0. left. left. apply H0. right. left. apply H0. Defined.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)