proposition: Lemma mapoL_mapsto l acc x v' : InA O.eqke (x,v') (mapoL f l acc) <-> (exists y v, y == x /\ List.In (y,v) l /\ f y v = Some v') \/ InA O.eqke (x,v') acc.
proof: Proof. revert acc. induction l as [|(k,e) l IH]; simpl; intros. - firstorder. - destruct (f k e) eqn:Hf; simpl in *; rewrite IH; clear IH; auto. rewrite ?InA_cons. + firstorder; try red in H; try red in H0; simpl in *; subst. * left. exists k, e; autom. * injection H0 as <- <-. right; left. compute; split; autom. congruence. + firstorder. injection H0 as <- <-. congruence. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)