proposition: Lemma map2_sorted : forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m'), sort (@ltk elt'') (map2 m m').
proof: Proof. intros. rewrite <- map2_alt_equiv. unfold map2_alt. assert (H0:=combine_sorted Hm Hm'). set (l0:=combine m m') in *; clearbody l0. set (f':= fun p : oee' => f (fst p) (snd p)). assert (H1:=map_sorted (elt' := option elt'') H0 f'). set (l1:=map f' l0) in *; clearbody l1. clear f' f H0 l0 Hm Hm' m m'. induction l1. - simpl; auto. - inversion_clear H1. destruct a; destruct o; auto. simpl. constructor; auto. clear IHl1. induction l1. + simpl; auto. + destruct a; destruct o; simpl; auto. * inversion_clear H0; auto. * inversion_clear H0. red in H1; simpl in H1. inversion_clear H. apply IHl1; auto. apply Inf_lt with (t1, None (A:=elt'')); auto. Qed.
imports: FMapInterface