proposition: Lemma sec_nullary_left : forall (X : Type) (q : WFT X) (s : WFT X) (R : X -> X -> Prop), SecureBy R q -> SecureBy R (oplus_nullary 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. simpl. apply H. apply H0. simpl. intro x. apply H. simpl in H0. apply H0. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)