proposition: Lemma sec_nullary_right : forall (X : Type) (q : WFT X) (s : WFT X) (R : X -> X -> Prop), SecureBy R s -> SecureBy R (oplus_nullary q s).
proof: Proof. intros X q. induction q. intros. simpl. apply H. intros. induction s. simpl. intros. apply H. simpl in H0. simpl. intros. left. apply H0. simpl. intro x. simpl in H0. remember (H0 x) as G0. apply H. simpl. intros. eapply sec_strengthen. 2: apply H0. intros. simpl in H2. destruct H2. left. left. apply H2. right. left. apply H2. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)