proposition: Lemma in_map_iff : forall (A B : Type) (f : A -> B) l b, LIn b (map f l) <=> {a : A $ LIn a l # b = f a}.
proof: Proof. induction l; simpl; sp; try (complete (split; sp)). trw IHl; split; sp; subst; sp. exists a; sp. exists a0; sp. right; exists a0; sp. Qed.
imports: UsefulTypes bin_rels Omega