proposition: Fact imsell_tps_mult_mono (X1 X2 Y1 Y2 : _ -> Prop) : X1 ⊆ X2 -> Y1 ⊆ Y2 -> X1⊛Y1 ⊆ X2⊛Y2.
proof: Proof. intros H1 H2 x (y & z & H3 & H4 & H5); subst. exists y, z; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)