proposition: Fact S_ill_restr_full_wc : S_ill_restr_wc ⇒ S_ill_wc.
proof: Proof. induction 1. all: try now constructor. + now constructor 2 with A. + now constructor 3 with (Γ := Γ). Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)