proposition: Lemma sec_left_sum_tree (X Y:Type) (p : WFT X): forall (A : X -> X -> Prop), SecureBy A p -> SecureBy (left_sum_lift A) (left_sum_tree Y p).
proof: Proof. induction p. intros A Zsec. simpl in *. intros v w x y z. destruct x; (repeat (auto; firstorder)). destruct v; (repeat (auto; firstorder)). destruct w; (repeat (auto; firstorder)). destruct v; (repeat (auto; firstorder)). destruct w; (repeat (auto; firstorder)). intros. simpl. intro x. destruct x; repeat auto. eapply sec_strengthen. 2: { apply H. apply H0. } intros. destruct x0; repeat (auto; firstorder). destruct y; repeat (auto; firstorder). simpl in *. intro x. destruct x; repeat (auto; firstorder). eapply sec_strengthen. 2: { apply H. apply H0. } intros. destruct x0; repeat (auto;firstorder). destruct y0; repeat (auto;firstorder). Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)