proposition: Lemma secure_from_wf : SecureBy (fun x y => not (R y x)) (SUP af_tree).
proof: Proof. intro x. unfold af_tree. generalize (wfR x). induction a using Acc_ind_dep. simpl. intros y. destruct (decR y x). simpl. eapply SecureBy_mon; eauto. simpl; intros. intuition. simpl. intros. intuition auto. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)