proposition: Lemma sec_strengthen: forall (X:Type) (p : WFT X) (A B : X -> X -> Prop), (forall x y, A x y -> B x y) -> SecureBy A p -> SecureBy B p.
proof: Proof. intros X p. induction p. intros A B H H0. simpl in H0. simpl. auto. intros A B H0 H1. simpl in H1. simpl. intro x. remember (H1 x) as G. eapply H. 2: apply G. intros. simpl in H2. destruct H2. left. apply H0. apply H2. right. apply H0. apply H2. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)