fact: Fixpoint ill_tps_list Γ := match Γ with | ∅ => eq vec_zero | A::Γ => ⟦A⟧ ** [[Γ]] end where "[[ Γ ]]" := (ill_tps_list Γ).
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)