proposition: Theorem S_ill_wc_weak_cntr Σ Γ A B : In A Σ -> ‼Σ++Γ ⊢ B <-> !A::‼Σ++Γ ⊢ B.
proof: Proof. revert Σ Γ; intros Si Ga. intros H. apply In_perm in H. destruct H as (Si' & H). split. + apply in_ill4_weak. + intros H1. apply in_ill4_perm with (‼(A :: Si') ++ Ga). * apply Permutation_app; auto. apply Permutation_map; auto. * simpl; apply in_ill4_cntr. revert H1; apply in_ill4_perm. simpl; apply Permutation_cons; auto. change (!A::‼Si'++Ga) with (‼(A::Si')++Ga). apply Permutation_app; auto. apply Permutation_map, Permutation_sym; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)