proposition: Fact imsell_perm_tps Γ Δ : Γ ~p Δ -> forall A, [< Γ |- A >] ⊆ [< Δ |- A >].
proof: Proof. intros H1 B x; unfold imsell_sequent_tps. intros H2 ? H3; apply H2; revert H3. apply imsell_tps_perm, Permutation_sym; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)