proposition: Lemma Lget_map : forall (A B:Set) (f:A -> B) i l, Lget i (List.map f l) = match Lget i l with Some a => Some (f a) | None => None end.
proof: Proof. induction i;intros [ | x l ] ;trivial. simpl;auto. Qed.
imports: List BinPos