proposition: Lemma SecureBy_mon p (R' S : X -> X -> Prop) (H : forall x y, R' x y -> S x y) : SecureBy R' p -> SecureBy S p.
proof: Proof. revert R' S H. induction p. simpl. intros. apply H. apply H0. simpl. intros. eapply H. 2:apply H1. intros. simpl in H2. intuition. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)