proposition: Lemma revmap_fold_helper: forall (A A' : Type) (f : A -> A') (a : A) (vv : list A) (base : list A'), revmap f (a :: vv) ++ base = revmap f vv ++ f a :: base.
proof: Proof. unfold revmap; intros; simpl. rewrite map_rev. rewrite map_app. simpl. rewrite <- app_assoc. simpl. rewrite <- map_rev. reflexivity. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs