proposition: Fact tile_concat_itau ln lt : tile_concat ln lt = (itau1 lt (rev ln), itau2 lt (rev ln)).
proof: Proof. induction ln as [ | i ln IH ]; simpl; auto. rewrite itau1_app, itau2_app; simpl. generalize (nth i lt ([], [])); intros (a,b); rewrite IH. repeat rewrite app_nil_r; auto. Qed.
imports: List Arith Lia Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs bsm_utils bsm_pcp) Undecidability.PCP(PCP PCP_facts)