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