proposition: Fact length_compiler_app ll mm : length_compiler (ll++mm) = length_compiler ll + length_compiler mm.
proof: Proof. induction ll as [ | x ll IH ]; simpl; auto. rewrite IH; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)