proposition: Fact lb_mask_equiv_app l m a b : length l = length m -> l ≂ m -> a ≂ b -> l++a ≂ m++b.
proof: Proof. intros H (? & ?) (? & ?); split; apply lb_mask_app; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)