proposition: Lemma combine_app: forall {A B: Type} (la1 la2: list A) (lb1 lb2: list B), length la1 = length lb1 -> combine (la1 ++ la2) (lb1 ++ lb2) = combine la1 lb1 ++ combine la2 lb2.
proof: Proof. intros. revert lb1 H; induction la1; intros; destruct lb1; try now inversion H. inv H. simpl. f_equal. apply IHla1; auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver