proposition: Lemma secure_by_power R p (H : SecureBy R p) k : SecureBy R (secure_power k p).
proof: Proof. induction k in R, p, H |- *; trivial. induction p. simpl in *. intros. apply IHk. simpl. intuition. simpl. intros. apply IHk. simpl. intros. simpl in H0. simpl in H. specialize (H x0). eapply SecureBy_mon. 2:eauto. simpl. intuition. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)