proposition: Fact lb_pointwise_sym l m : (forall x y, f x y = f y x) -> lb_pointwise l m = lb_pointwise m l.
proof: Proof. intros H; revert l m; induction l as [ | x l IHl ]; intros m. + rewrite lb_pointwise_left, lb_pointwise_right. apply map_ext; intro; auto. + destruct m as [ | y m ]. * rewrite lb_pointwise_left, lb_pointwise_right. apply map_ext; intro; auto. * do 2 rewrite lb_pointwise_cons; f_equal; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)