proposition: Lemma sec_right_sum_tree (X Y:Type) (p : WFT Y) : forall (B : Y -> Y -> Prop), SecureBy B p -> SecureBy (right_sum_lift B) (right_sum_tree X p).
proof: Proof. intros. unfold right_sum_lift. apply cofmap_secures. apply sec_left_sum_tree; assumption. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)