proposition: Lemma fold1_elements': forall (A B: Type) (f: B -> A -> B) (m: ptrie A) (v: B), fold1' f m v = List.fold_left (fun a p => f a (snd p)) (elements' m nil) v.
proof: Proof. induction m; intros; auto. simpl. replace (elements' m2 nil) with (nil ++ elements' m2 nil); auto. rewrite elements_append'. rewrite fold_left_app. rewrite IHm1. auto. Qed.
imports: Lia Cdcl.Coqlib