proposition: Fact imsell_sequent_tps_mono Γ A B : ⟦A⟧ ⊆ ⟦B⟧ -> [< Γ |- A >] ⊆ [< Γ |- B >].
proof: Proof. intros H x; simpl; unfold imsell_sequent_tps. intros H1 ? H2; apply H, H1; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)