proposition: Lemma sec_unary_left : forall (X : Type) (q : WFT X) (s : WFT X) (R : X -> X -> Prop), SecureBy R q -> SecureBy R (oplus_unary q s).
proof: Proof. intros X q. induction q. intros. simpl in H. simpl. induction s. simpl. apply H. simpl. intro x. eapply sec_strengthen. 2: apply H0. intros. left. apply H1. intros. induction s. simpl. simpl in H0. intro x. apply H0. simpl. intro x. apply sec_nullary_left. apply H. simpl in H0. apply H0. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)