proposition: Lemma ins_spec : forall s x y, InT y (ins x s) <-> X.eq y x \/ InT y s.
proof: Proof. induct s x. - intuition_in. - intuition_in. setoid_replace y with x; eauto. - descolor; autorew; rewrite IHl; intuition_in. - descolor; autorew; rewrite IHr; intuition_in. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat