proposition: Fact imsell_tps_imp_zero X Y : (X -⊛ Y) ⦳ <-> X ⊆ Y.
proof: Proof. split. + intros ? ? ?; rewrite <- vec_zero_plus, vec_add_comm; auto. + intros ? ?; rewrite vec_add_comm, vec_zero_plus; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)