fact: Fixpoint SecureBy (R : X -> X -> Prop) (p : WFT) : Prop := match p with | ZT => forall x y, R x y | SUP f => forall x, SecureBy (fun y z => R y z \/ R x y) (f x) end.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)