proposition: Fact imsell_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 (? & ? & ? & ? & ?); subst; auto; rewrite vec_zero_plus; auto. + destruct Hx as (y & z & H1 & H2 & H3). apply IH in H3. destruct H3 as (c & d & H4 & H5 & H6). exists (vec_plus y c), d; split. * subst; apply vec_add_assoc. * split; auto. exists y, c; auto. + destruct Hx as (y & d & ? & (z & g & ? & ? & ?) & ?). exists z, (vec_plus g d); split. * subst; symmetry; apply vec_add_assoc. * split; auto. apply IH. exists g, d; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)