fact: Fixpoint imsell_tps_list Γ := match Γ with | nil => eq ⦳ | A::Γ => ⟦A⟧⊛⟪Γ⟫ end where "⟪ Γ ⟫" := (imsell_tps_list Γ).
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)