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 := t0::l). set (u := last us default). case_eq (subterm_pos u p). 2: discr. intro v. case_eq (matches t v); intros. 2: discr. assert (h0 : k us > 0). unfold k, us. simpl. lia. assert (h : u = last_term us). unfold last_term, k, nth. rewrite <- last_nth. refl. rewrite h in H0. exists (seq us h0 p H0 t1). eapply IS_seq. apply H1. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil ATrs ListUtil RelUtil AMatching ListDec APosition NatUtil)