proposition: Fact decoder_length s i lt : length (decoder s i lt) = length_decoder lt.
proof: Proof. revert s i; induction lt as [ | (th,tl) lt IHlt ]; intros s i; rew length; auto. simpl; rew length; rewrite IHlt; lia. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)