proposition: Fact imsell_tps_bang_U u A : U u -> (forall v, ⟦![u]A⟧ v <-> v = ⦳) <-> ⟦A⟧ ⦳.
proof: Proof. Proof using HK_unit0 HK_unit1. intros Hu; split. + intros H; rewrite <- imsell_tps_bang_zero, H; auto. + intros H v; split; simpl. * intros (_ & H1); revert H1; eauto. * intros ->; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)