proposition: Fact full_decoder_length i ll : length (full_decoder i ll) = length_full_decoder ll.
proof: Proof. unfold full_decoder, length_full_decoder; rew length; rewrite decoder_length; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)