proposition: Lemma oplus_unary_sec_intersection {X} (p q : WFT X) (C : X -> X -> Prop) (A B : X -> Prop) : SecureBy (fun y z => C y z \/ A y) p -> SecureBy (fun y z => C y z \/ B y) q -> SecureBy (fun y z => C y z \/ (A y /\ B y)) (oplus_unary p q).
proof: Proof. funelim (oplus_unary p q); simpl; intros. - eapply SecureBy_mon; [|eapply H0]; simpl; firstorder. - eapply SecureBy_mon; [|eapply H]. simpl; firstorder. - eapply SecureBy_mon. 2:eapply (oplus_nullary_sec_intersection _ _ _ (A x) (B x)). simpl. intros. destruct H3; [|intuition auto]. rewrite <- or_assoc. left. eapply H3. -- simpl. eapply SecureBy_mon; [|eapply (H _ (fun y z => C y z \/ C x y \/ A x) A B)]. simpl. intuition auto. eapply SecureBy_mon; [|eapply H1]; simpl. intros. intuition auto. simpl. intros. eapply SecureBy_mon; [|eapply H2]; simpl. intros. intuition auto. -- simpl. specialize (H0 x (SUP f) (g x)). eqns_specialize_eqs H0. eapply SecureBy_mon; [|eapply (H0 (fun y z => C y z \/ C x y \/ B x) A B)]; simpl. intuition auto. intuition. simpl in H2. eapply SecureBy_mon; [|eapply H1]; simpl. intuition auto. eapply SecureBy_mon; [|eapply H2]; simpl. intros. intuition auto. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)