proposition: Fact ill_tps_app Γ Δ x : [[Γ++Δ]] x <-> ([[Γ]]**[[Δ]]) x.
proof: Proof. revert Γ Δ x; intros Ga De. induction Ga as [ | A Ga IH ]; intros x; simpl; split; intros Hx. + exists vec_zero, x; simpl; rew vec. + destruct Hx as (a & b & H1 & H2 & H3); subst; auto; rewrite vec_zero_plus; auto. + destruct Hx as (a & b & H1 & H2 & H3). apply IH in H3. destruct H3 as (c & d & H4 & H5 & H6). exists (vec_plus a c), d; split. * subst; apply vec_add_assoc. * split; auto. exists a, c; auto. + destruct Hx as (y & d & H1 & H2 & H3). destruct H2 as (a & g & H2 & H4 & H5). exists a, (vec_plus g d); split. * subst; symmetry; apply vec_add_assoc. * split; auto. apply IH. exists g, d; auto. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)