proposition: Lemma xmap2_lr : forall (A B : Type)(f g: option A -> option A -> option B)(m : t A), (forall (i j : option A), f i j = g j i) -> xmap2_l f m = xmap2_r g m.
proof: Proof. induction m; intros; simpl; auto. rewrite IHm1; auto. rewrite IHm2; auto. rewrite H; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface