proposition: Lemma gmap: forall {A B : Type} (l: list A) (f : forall a, LIn a l -> B), list B.
proof: Proof. induction l as [| a l maprec]; introv f. exact nil. pose proof f a as Hb. lapply Hb;[ intro b | left; auto]. assert ( forall a0 : A, LIn a0 (l) -> B) as frec. introv Hin. eapply f. right. eauto. pose proof (maprec frec) as brec. exact (b::brec). Defined.
imports: UsefulTypes bin_rels Omega