proposition: Lemma ext' n: forall a b, a<pow2 n -> b<pow2 n -> (forall i, i<n -> mem' n a i = mem' n b i) -> a = b.
proof: Proof. induction n; simpl; intros a b Ha Hb H. rewrite lt_n_1 by assumption. now apply lt_n_1. apply od_inj. revert H. generalize (od_bound _ _ Ha), (od_bound _ _ Hb). case od. intros oa a' Ha'. case od. intros ob b' Hb'. intro H. f_equal. apply (H 0 eq_refl). apply IHn; trivial. intros i Hi. apply (H (S i) Hi). Qed.
imports: List PeanoNat common comparisons