proposition: Lemma mem_of_fun n (f: ord n -> bool) i: mem (of_fun f) i = f i.
proof: Proof. unfold mem, of_fun. simpl. rewrite mem_of_fun' by apply ord_lt. unfold app'. case lt_ge_dec. intros. f_equal. now apply eq_ord. rewrite (ord_lt i). discriminate. Qed.
imports: List PeanoNat common comparisons