proposition: Lemma lin_lift: forall {A B:Type} (a:A) (lv: list A) (f:A->B), LIn a lv -> LIn (f a) (map f lv).
proof: Proof. induction lv as [| v lv Hind] ; [sp | ]; introv Hin. simpl. dorn Hin;subst;spc. Qed.
imports: UsefulTypes bin_rels Omega