proposition: Lemma wf_parent : forall c0 : Config, legal c0 -> well_founded (parent c0).
proof: Proof. intros; apply wf_R with (f := dt c0). intros; apply parent_cr; trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc