proposition: Lemma firstn_length {A} : forall (l l': list A), l = (firstn (length l) (l ++ l')).
proof: Proof. induction l. - reflexivity. - simpl; intros; rewrite <- IHl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List Bedrock.Platform.Facade.examples.QsADTs