proposition: Theorem imemo_get_correct: forall n, memo_get n imemo_list = f n.
proof: Proof. assert (F1: forall n m, memo_get n (imemo_make (f m)) = f (S (n + m))). { induction n as [| n Hrec]; try (intros m; exact (eq_sym (Hg_correct m))). simpl; intros m; rewrite <- Hg_correct, Hrec, <- plus_n_Sm; auto. } destruct n as [| n]; try reflexivity. unfold imemo_list; simpl; rewrite F1. rewrite <- plus_n_O; auto. Qed.
imports: Eqdep_dec Streams