proposition: Fact S_ill_restr_cntr Γ Δ B : ‼Γ++‼Γ++Δ ⊢r B -> ‼Γ++ Δ ⊢r B.
proof: Proof. revert Γ Δ; intros Ga. induction Ga as [ | A Ga IH ]; simpl; auto; intros De. intros H. apply in_ill1_cntr. apply in_ill1_perm with (‼Ga ++ (!A::!A::De)). + apply Permutation_sym. do 2 apply Permutation_cons_app; auto. + apply IH. revert H; apply in_ill1_perm. rewrite app_assoc. apply Permutation_cons_app. rewrite <- app_assoc. apply Permutation_app; auto. apply Permutation_cons_app; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)