proposition: Lemma ext n (a b: ord (pow2 n)): (forall i, mem a i = mem b i) -> a = b.
proof: Proof. intro H. apply eq_ord. eapply ext'. apply ord_lt. apply ord_lt. intros i Hi. apply (H (Ord i Hi)). Qed.
imports: List PeanoNat common comparisons