proposition: Lemma map_induction_bis : forall P : t elt -> Type, (forall m m', m == m' -> P m -> P m') -> P empty -> (forall x e m, ~In x m -> P m -> P (add x e m)) -> forall m, P m.
proof: Proof. intros. apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)