fact: Fixpoint ill_tps A x : Prop := match A with | £ X => s X x | A & B => ⟦A⟧ x /\ ⟦B⟧ x | !A => ⟦A⟧ x /\ x = vec_zero | A ⊸ B => (⟦A⟧ -* ⟦B⟧) x | A ⊗ B => (⟦A⟧ ** ⟦B⟧) x | A ⊕ B => ⟦A⟧ x \/ ⟦B⟧ x | ⟘ => False | ⟙ => True | _ => x = vec_zero end where "⟦ A ⟧" := (ill_tps A).
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)