proposition: Lemma sec_bool : SecureBy eq bool_tree.
proof: Proof. simpl. intros x y. destruct x; repeat (simpl;auto). destruct y; repeat (simpl;auto). intros x y z. destruct x; repeat (simpl; auto). destruct y; repeat (simpl; auto). intros x y z. destruct x; repeat (simpl; auto). Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)