proposition: Fact ill_tps_list_bang_zero Γ : [[‼Γ]] vec_zero <-> forall A, In A Γ -> ⟦A⟧ vec_zero.
proof: Proof. induction Γ as [ | A Ga IH ]. + split. * simpl; tauto. * intros _; simpl; auto. + split. * intros (u & v & H1 & H2 & H3). destruct H2 as [ H2 H4 ]; subst; auto. rewrite vec_zero_plus in H1; subst. rewrite IH in H3. intros B [ E | HB ]; subst; auto. * intros H. exists vec_zero, vec_zero. rewrite vec_zero_plus; repeat split; auto. - apply H; left; auto. - rewrite IH. intros; apply H; right; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)