proposition: Fact ill_sequent_tps_mono Γ A B : (forall x, ⟦A⟧ x -> ⟦B⟧ x) -> forall x, [< Γ |- A >] x -> [< Γ |- B >] x.
proof: Proof. intros H x; simpl; unfold ill_sequent_tps. intros H1 a H2. apply H, H1; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)