proposition: Lemma ble_1: forall S1 S2, ble S1 S2 = true -> le S1 S2.
proof: Proof. unfold ble, le; intros. destruct S1 as [ | m1]. - elim (V.bot_1 (s "")). apply H0. - destruct S2 as [ | m2]. discriminate. red; cbn; intros. destruct (IdentMap.find x m2) as [N2|] eqn:F2. + apply IdentMap.find_2 in F2. eapply IMProp.for_all_iff in H; eauto. apply V.ble_1 in H. apply H. apply H0. hnf. intros; subst x0. hnf; intros. subst x0. auto. + apply V.top_1. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)