proposition: Lemma combine_app_distrib {A B} : forall (l1 l1' : list A) (l2 l2' : list B), List.length l1 = List.length l2 -> combine (app l1 l1') (app l2 l2') = app (combine l1 l2) (combine l1' l2').
proof: Proof. induction l1; destruct l2; simpl; intros; try discriminate. - reflexivity. - rewrite IHl1; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction