proposition: Theorem ptree_merge_pairs_correct : forall p l, permut (ptree_to_list (ptree_merge_pairs p l)) (ptree_to_list p ++ flat_map ptree_to_list l).
proof: Proof. intros p l. revert p. induction l as [|v|v w l IH] using list_ind2 ; simpl ; intros p. rewrite app_nil_r. apply permut_refl. rewrite app_nil_r. apply ptree_meld_correct. eapply permut_trans. apply ptree_meld_correct. rewrite app_assoc. eapply permut_trans. apply permut_app_r. apply ptree_meld_correct. now apply permut_app_l. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)