proposition: Lemma fixpoint_eq: eq fixpoint (F fixpoint).
proof: Proof. assert (REC: forall x acc PRE, eq (iterate x acc PRE) (F (iterate x acc PRE))). { induction x using (well_founded_induction gt_wf). intros. destruct acc; cbn. destruct (eq_dec x (F x)). - auto. - apply H. split; auto. } apply REC. Qed.
imports: Coq(Extraction ExtrOcamlBasic)