proposition: Lemma sup_rewrite: forall (X:Type) (A : X -> X -> Prop) (f : X -> WFT X), SecureBy A (SUP f) = forall x, SecureBy (fun y z => A y z \/ A x y) (f x).
proof: Proof. intros; auto. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)