proposition: Theorem S_imsell_extract Γ u A B : ![u]A ∊ Γ -> U u -> Γ ⊢ B <-> ![u]A::Γ ⊢ B.
proof: Proof. intros H1 H2; split. + apply in_imsell_weak; auto. + intros H3. apply In_perm in H1 as (Δ & H1). apply in_imsell_perm with (1 := H1). apply in_imsell_cntr; auto. apply in_imsell_perm with (2 := H3). apply perm_skip, Permutation_sym; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)