proposition: Fact S_imsell_weak Γ Δ B : Forall (fun '(u,_) => U u) Γ -> Δ ⊢ B -> ‼Γ++Δ ⊢ B.
proof: Proof. intros H1 H2; revert H1. induction 1 as [ | (u,A) Γ H1 IH1 ]; simpl; auto. apply in_imsell_weak; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)