fact: Fixpoint mem' n x := match n with | 0 => fun i => assert_false false | S n => let (o,x) := od x in let f := mem' n x in fun i => match i with O => o | S i => f i end end.
imports: List PeanoNat common comparisons