proposition: Lemma lenth_combine {A B} : forall (l1 : list A) (l2 : list B), List.length l1 = List.length l2 -> List.length (combine l1 l2) = List.length l1 /\ List.length (combine l1 l2) = List.length l2.
proof: Proof. induction l1; destruct l2; simpl; intros; try discriminate; intuition. - erewrite (fun H => proj1 (IHl1 l2 H)); congruence. - erewrite (fun H => proj2 (IHl1 l2 H)); congruence. 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