proposition: Lemma widen_order_wf: well_founded widen_order.
proof: Proof. assert (A: forall m, Acc widen_order (Top_except m)). { induction m using (well_founded_ind (well_founded_ltof _ measure_map)). constructor. intros S (S2 & EQ & BLE). subst S. destruct S2. discriminate. apply H. apply measure_widen_lt. auto. } assert (B: Acc widen_order Bot). { constructor. intros S (S2 & EQ & BLE). subst S. unfold ble in BLE. destruct S2. discriminate. apply A. } red. destruct a; auto. Defined.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)