proposition: Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n.
proof: Proof. intros n; unfold dmemo_get, dimemo_list. rewrite (imemo_get_correct memo_val mf mg); simpl. - case (is_eq n n); simpl; auto; intros e. assert (e = eq_refl n). + apply eq_proofs_unicity. induction x as [| x Hx]; destruct y as [| y]. * left; auto. * right; intros HH; discriminate HH. * right; intros HH; discriminate HH. * case (Hx y). -- intros HH; left; case HH; auto. -- intros HH; right; intros HH1; case HH. injection HH1; auto. + rewrite H; auto. - intros n1; unfold mf; rewrite Hg_correct; auto. Qed.
imports: Eqdep_dec Streams