proposition: Theorem ltStateWf : well_founded ltState.
proof: Proof. unfold ltState in |- *; apply wf_inverse_image with (B := nat); auto with stalmarck. try exact lt_wf. Qed.
imports: Stalmarck(state) Coq(Arith) Stalmarck(stateDec) Coq(Inverse_Image) Coq(Compare) Coq(Relation_Definitions)