proposition: Remark loopexec : forall s : St, Invar s -> {s' : St | Invar s' /\ LoopExit s'}.
proof: Proof. refine (well_founded_induction Termi (fun s => _) (fun s hr i => match LoopExit_dec s i with | left _ => exist _ s _ | right _ => match Onestep s _ _ with | exist s' h' => match hr s' _ _ with | exist s'' _ => exist _ s'' _ end end end)); auto; elim h'; auto. Qed.