proposition: Theorem memo_get_correct: forall n, memo_get n memo_list = f n.
proof: Proof. assert (F1: forall n m, memo_get n (memo_make m) = f (n + m)). { induction n as [| n Hrec]; try (intros m; reflexivity). intros m; simpl; rewrite Hrec. rewrite plus_n_Sm; auto. } intros n; transitivity (f (n + 0)); try exact (F1 n 0). rewrite <- plus_n_O; auto. Qed.
imports: Eqdep_dec Streams