proposition: Lemma sec_sum_lift (X Y : Type) : forall (A : X -> X -> Prop) (B : Y -> Y -> Prop) (p : WFT X) (q : WFT Y), SecureBy A p -> SecureBy B q -> SecureBy (sum_lift A B) (oplus_binary (left_sum_tree Y p) (right_sum_tree X q)).
proof: Proof. intros A B p q Asec Bsec. apply sec_strengthen with (A := fun x y => left_sum_lift A x y /\ right_sum_lift B x y). intros x y. destruct x; destruct y; repeat firstorder. apply oplus_binary_sec_intersection. apply sec_left_sum_tree; assumption. apply sec_right_sum_tree; assumption. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)