proposition: Fact imsell_sequent_tps_eq Γ A : [< Γ |- A >] ⦳ <-> ⟪Γ⟫ ⊆ ⟦A⟧.
proof: Proof. split. * intros H x Hx. rewrite <- vec_zero_plus, vec_add_comm. apply (H x); trivial. * intros H x Hx. rewrite vec_add_comm, vec_zero_plus; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)