proposition: Lemma oplus_nullary_sec_intersection {X} (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. revert C q. induction p; simpl; intros; auto. induction q in C, H, H0 |- *; simpl in *; intuition. specialize (H x y). specialize (H0 x y). intuition. specialize (H1 x (fun y z => (C y z \/ A /\ B) \/ C x y)). simpl in *. eapply SecureBy_mon. 2:eapply H1. simpl. intuition. intuition. firstorder auto. eapply SecureBy_mon. 2:eapply H0. simpl. firstorder auto. specialize (H x (fun y z => C y z \/ C x y)). simpl in *. eapply SecureBy_mon. 2:eapply H. all:simpl. intros. firstorder auto. eapply SecureBy_mon. 2:eapply H0. simpl. intros. intuition. eapply SecureBy_mon. 2:eapply H1. simpl. intros. intuition. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)