proposition: Lemma set_1: forall x n N s S, V.In n N -> In s S -> In (update x n s) (set x N S).
proof: Proof. unfold In, get, set; intros. destruct (V.ble N V.bot) eqn:BLE; [ | destruct S ]. - apply V.ble_1 in BLE. apply BLE in H. elim (V.bot_1 n); auto. - elim (V.bot_1 (s "")). auto. - rewrite IMFact.add_o. change IdentMap.E.eq_dec with string_dec. unfold update. destruct (string_dec x x0); auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)