proposition: Lemma xbindings_spec: forall m j acc k e, InL (k,e) (xbindings m j acc) <-> InL (k,e) acc \/ exists x, k=(j@x) /\ find x m = Some e.
proof: Proof. induction m as [|l IHl o r IHr]; simpl. - intros. split; intro H. + now left. + destruct H as [H|[x [_ H]]]. assumption. now rewrite gleaf in H. - intros j acc k e. case o as [e'|]; rewrite IHl, ?InA_cons, IHr; clear IHl IHr; split. + intros [[H|[H|H]]|H]; auto. * change (E.eq k (rev j) /\ e = e') in H. destruct H as (->,<-). right. now exists 1. * destruct H as (x,(->,H)). right. now exists x~1. * destruct H as (x,(->,H)). right. now exists x~0. + intros [H|H]; auto. destruct H as (x,(->,H)). destruct x; simpl in *. * left. right. right. now exists x. * right. now exists x. * left. left. injection H as ->. reflexivity. + intros [[H|H]|H]; auto. * destruct H as (x,(->,H)). right. now exists x~1. * destruct H as (x,(->,H)). right. now exists x~0. + intros [H|H]; auto. destruct H as (x,(->,H)). destruct x; simpl in *. * left. right. now exists x. * right. now exists x. * discriminate. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)