proposition: Fact S_ill_restr_weak Γ Δ B : Δ ⊢r B -> ‼Γ++Δ ⊢r B.
proof: Proof. intro; induction Γ; simpl; auto; apply in_ill1_weak; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)