proposition: Lemma is_mod_loop_correct : forall t mds ds p, is_mod_loop t mds ds p = true -> EIS (red_mod E R).
proof: Proof. intros t mds ds p. unfold is_mod_loop. case_eq (mod_rewrites t mds). 2: discr. destruct l. discr. set (us := t0::l). set (u := last us default). case_eq (rewrites E u ds). 2: discr. intro us'. set (u' := last us' u). 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. unfold u' in H0. rewrite h in H0. exists (seq us h0 us' p H0 t1). eapply IS_seq. apply H2. rewrite h in H1. apply H1. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(ATrs LogicUtil ALoop ListUtil RelUtil NatUtil APosition AMatching ARelation)