proposition: Fact S_imsell_gen_weak u Γ Δ B : U u -> Δ ⊢ B -> map (fun A => ![u]A) Γ++Δ ⊢ B.
proof: Proof. intros H1 H2. replace (map (fun A => ![u]A) Γ) with (‼ (map (fun A => (u,A)) Γ)). + apply S_imsell_weak; auto. apply Forall_forall. intros ?; rewrite in_map_iff. intros (? & <- & ?); auto. + unfold imsell_lban; rewrite map_map; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)