proposition: Fact imsell_tps_perm Γ Δ : Γ ~p Δ -> ⟪Γ⟫ ⊆ ⟪Δ⟫.
proof: Proof. induction 1 as [ | A Ga De H IH | A B Ga | ]; simpl; auto. + intros x (y & z & H1 & H2 & H3). exists y, z; repeat split; auto. + intros x (y & z & H1 & H2 & c & d & H3 & H4 & H5). exists c, (vec_plus y d); split. * subst; rewrite (vec_add_comm c), vec_add_assoc, (vec_add_comm c); auto. * split; auto. exists y, d; auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)