proposition: Fact ll_tps_mult_mono (X1 X2 Y1 Y2 : _ -> Prop) : (forall x, X1 x -> X2 x) -> (forall x, Y1 x -> Y2 x) -> (forall x, (X1**Y1) x -> (X2**Y2) x).
proof: Proof. intros H1 H2 x (a & b & H3 & H4 & H5); subst. exists a, b; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)