proposition: Lemma oplus_binary_sec_intersection {X} (p q : WFT X) (A B : X -> X -> Prop) : SecureBy A p -> SecureBy B q -> SecureBy (fun y z => A y z /\ B y z) (oplus_binary p q).
proof: Proof. revert p q A B; intros p q. funelim (oplus_binary p q); simpl; intros. eapply SecureBy_mon. 2:eapply H0. simpl. firstorder. eapply SecureBy_mon; [|eapply H]. simpl; firstorder. eapply SecureBy_mon. 2:eapply (oplus_unary_sec_intersection _ _ _ (A x) (B x)). simpl. intros. destruct H3; [|intuition auto]. left. eapply H3. - simpl. eapply SecureBy_mon; [|eapply (H _ (fun y z => A y z \/ A x y) B)]; simpl. unfold sec_disj. 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 A (fun y z => B y z \/ B x y))]; simpl. intuition auto. intuition. simpl in H2. apply H2. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)