proposition: Theorem imsell_tps_sound Γ A : Γ ⊢ A -> [< Γ |- A >] ⦳.
proof: Proof. Proof using All. induction 1 as [ A | Γ Δ A H1 H2 IH2 | Γ Δ A B C H1 IH1 H2 IH2 | Γ A B H1 IH1 | Γ m A B H1 IH1 | Γ m A H1 H2 IH2 | Γ u A B H1 H2 IH2 | Γ u A B H1 H2 IH2 ]; unfold imsell_sequent_tps in * |- *. + intros x; simpl; intros (y & z & H1 & H2 & H3); subst; eq goal H2. f_equal; do 2 rewrite vec_add_comm, vec_zero_plus; auto. + revert IH2; apply imsell_perm_tps; auto. + intros x (y & z & H3 & H4 & H5); simpl. apply IH2. apply imsell_tps_app in H5 as (g & d & H5 & H6 & H7). simpl in H4; apply IH1, H4 in H6. exists (vec_plus y g), d; repeat split; auto. * subst; apply vec_add_assoc. * eq goal H6; f_equal; rew vec. + simpl; intros y Hy x Hx. rewrite vec_add_assoc. apply IH1. exists x, y; repeat split; auto. + intros x (y & z & H2 & H3 & H4). apply IH1; exists y, z; repeat split; auto. apply H3. + intros x Hx; split. * apply IH2; auto. * rew vec. revert Hx; apply imsell_tps_lbang; auto. + intros x (y & z & -> & H3 & H4); rew vec. apply proj2, HK_unit1 in H3; auto; subst. rewrite vec_add_comm. now apply IH2. + intros x (y & z & G2 & G3 & G4). apply IH2. exists y, z; repeat (split; auto). exists y, z; repeat (split; auto). apply proj2, HK_unit1 in G3; auto. subst; rew vec; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)