proposition: Lemma is_loop_correct : forall t ds p, is_loop t ds p = true -> EIS (red R).
proof: Proof. intros t ds p. unfold is_loop. case_eq (rewrites t ds). 2: discr. destruct l. discr. set (us := s::l). set (u := last us default). case_eq (split u p). 2: discr. intros [v w]. case_eq (matches t w); intros. 2: discr. assert (h0 : k us > 0). unfold k, us. simpl. lia. assert (h : u = last_string us). unfold last_string, k, nth. rewrite <- last_nth. refl. rewrite h in H0. exists (seq us h0 v s0). eapply IS_seq. apply H1. apply H0. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)