proposition: Lemma codelen_app: forall c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2.
proof: Proof. induction c1; intros. - auto. - cbn [app]. rewrite ! codelen_cons. rewrite IHc1. lia. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)