proposition: Lemma oplus_binary_sec_intersection' {X} (p q : WFT X) (C : X -> X -> Prop) (A B : X -> X -> Prop) : SecureBy (fun y z => C y z \/ A y z) p -> SecureBy (fun y z => C y z \/ B y z) q -> SecureBy (fun y z => C y z \/ (A y z /\ B y z)) (oplus_binary p q).
proof: Proof. 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]. rewrite <- or_assoc. left. eapply H3. - simpl. eapply SecureBy_mon; [|eapply (H _ (fun y z => C y z \/ C x y \/ A x y) 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 y) 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. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)