proposition: Lemma mem_of_fun' n: forall f i, i<n -> mem' n (of_fun' n f) i = f i.
proof: Proof. induction n; intros f i Hi; simpl. destruct i; discriminate. case_eq (f 0); intro H. rewrite od_xI. destruct i. congruence. now rewrite IHn. rewrite od_xO. destruct i. congruence. now rewrite IHn. Qed.
imports: List PeanoNat common comparisons