proposition: Fact imsell_tps_bang_zero m A : ⟦![m]A⟧ ⦳ <-> ⟦A⟧ ⦳.
proof: Proof. Proof using HK_unit0. simpl; split; auto; tauto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)