proposition: Lemma create_in : forall l x e r y, In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r.
proof: Proof. unfold create; split; [ inversion_clear 1 | ]; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int