fact: Fixpoint lb_pointwise l m := match l, m with | nil, nil => nil | _, nil => map (fun x => f x ⟘) l | nil, _ => map (f ⟘) m | x::l, y::m => f x y :: lb_pointwise l m end.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)