proposition: Lemma sec_binary_right : forall (X : Type) (q : WFT X) (s : WFT X) (R : X -> X -> Prop), SecureBy R s -> SecureBy R (oplus_binary q s).
proof: Proof. intros X q. induction q. intros. simpl. apply H. intros. induction s. simpl in H0. apply sec_binary_left. simpl. intros. remember (w x). clear Heqw0. induction w0. simpl. intros. left. apply H0. simpl. intro x0. eapply sec_strengthen. 2: apply H1. intros. simpl in H2. right. right. apply H0. simpl. intro x. apply sec_unary_left. apply H. eapply sec_strengthen. 2: apply H0. intros. left. apply H2. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)