proposition: Lemma oplus_nullary_sec_intersection: forall (X:Type) (p : WFT X) (q: WFT X) (C : X -> X -> Prop) (A : Prop) (B : Prop), SecureBy (fun y z => C y z \/ A) p -> SecureBy (fun y z => C y z \/ B) q -> SecureBy (fun y z => C y z \/ (A /\ B)) (oplus_nullary p q).
proof: Proof. intros X p. induction p. intros. simpl. simpl in H. eapply sec_strengthen. 2: apply H0. intros. simpl in H1. destruct H1. left. apply H1. destruct (H x y). left. apply H2. right. auto. intros. simpl. simpl in H0. intro x. remember (H0 x). remember (@H x q (fun y z => C y z \/ C x y) A B). eapply sec_strengthen. 2: { apply s0. clear Heqs. clear H0. eapply sec_strengthen. 2: apply s. intros. simpl in H0. destruct H0. destruct H0. left. left. apply H0. right. apply H0. destruct H0. left. right. apply H0. right. apply H0. subst. eapply sec_strengthen. 2: apply H1. intros. simpl in H2. destruct H2. left. left. apply H2. right. apply H2. } intros. simpl in H2. destruct H2. destruct H2. left. left. apply H2. right; left. apply H2. right. right. apply H2. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)