proposition: Fact ill_tps_lbang Γ x : [[‼Γ]] x <-> [[Γ]] x /\ x = vec_zero.
proof: Proof. revert Γ x; intros Ga. induction Ga as [ | A Ga IH ]; intros x. + simpl; split; auto; tauto. + split. * intros (a & g & H1 & H2 & H3). split. - exists a, g; repeat split; auto. ** apply H2. ** apply IH; auto. - apply IH, proj2 in H3. apply proj2 in H2; subst; auto. apply vec_zero_plus. * intros ((a & g & H1 & H2 & H3) & H4). exists x, x. assert (a = vec_zero /\ g = vec_zero) as E. { apply vec_plus_is_zero; subst; auto. } destruct E; subst; repeat split; auto; rew vec. apply IH; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)