proposition: Fact imsell_tps_list_zero Γ : (forall A, A ∊ Γ -> ⟦A⟧ ⦳) -> ⟪Γ⟫ ⦳.
proof: Proof. induction Γ as [ | A Γ IH ]; simpl; auto; intros H. exists ⦳, ⦳; msplit 2; auto; now rewrite vec_zero_plus. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)