proposition: Lemma app_inj : forall (A : Type) (l1 l1' l2 l2' : list A), List.length l1' = List.length l2' -> (l1' ++ l1)%list = (l2' ++ l2)%list -> l1' = l2' /\ l1 = l2.
proof: Proof. induction l1'; destruct l2'; simpl; intros; try discriminate; intuition. injections; eauto. destruct (IHl1' l2 l2'); eauto; subst; eauto. injections; eauto. destruct (IHl1' l2 l2'); eauto; subst; 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