proposition: Lemma chain_dp_hd_red_mod : forall a, chain_dp a << hd_red_mod R (a::nil).
proof: Proof. unfold inclusion. intros. destruct H. do 2 destruct H0. subst y. destruct a. simpl. simpl in H0. exists (sub x0 lhs). split. apply incl_elim with (R := int_red R #). apply rtc_incl. apply int_red_incl_red. exact H0. apply hd_red_rule. simpl. auto. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)