proposition: Lemma elements_branch': forall A (t1 t2: ptrie A) p m, elements' (Branch p m t1 t2) nil = elements' t1 nil ++ elements' t2 nil.
proof: Proof. intros; simpl. rewrite <- elements_append'. auto. Qed.
imports: Lia Cdcl.Coqlib