proposition: Theorem ptree_insert_correct : forall p v, permut (ptree_to_list (ptree_insert p v)) (v :: ptree_to_list p).
proof: Proof. intros [v1 l1] v. unfold ptree_insert. eapply permut_trans. apply ptree_meld_correct. apply (permut_app _ (v :: nil)). Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)