proposition: Lemma sec_union (X:Type) (A:X->X->Prop) (B:X->X->Prop): forall p, SecureBy A p -> SecureBy (fun x y => A x y \/ B x y) p.
proof: Proof. intros p Asec. eapply sec_strengthen. intros. left. apply H. apply Asec. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)