proposition: Fact S_imsell_cntr Γ Δ B : Forall (fun '(u,_) => U u) Γ -> ‼Γ++‼Γ++Δ ⊢ B -> ‼Γ++Δ ⊢ B.
proof: Proof. intros H; revert H Δ. induction 1 as [ | (u,A) Γ H1 H2 IH2 ]; simpl; auto; intros Δ H. apply in_imsell_cntr; auto. apply in_imsell_perm with (‼Γ ++ (![u]A::![u]A::Δ)). + apply Permutation_sym. do 2 apply Permutation_cons_app; auto. + apply IH2. revert H; apply in_imsell_perm. rewrite app_assoc. apply Permutation_cons_app. rewrite <- app_assoc. apply Permutation_app; auto. apply Permutation_cons_app; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)