proposition: Lemma dup_int_rules_int_red_rtc_aux : forall u t, red R # u t -> forall f v, u = Fun' (hd_symb f) v -> int_red R # u t /\ exists w, t = Fun' (hd_symb f) w.
proof: Proof. intros u t H. induction H; intros. assert (int_red R # x y). apply rt_step. rewrite H0. apply dup_int_rules_int_red. subst;auto. split. auto. clear H. ded (int_red_rtc_preserve_hd H1). destruct H. exists v. subst. auto. do 3 destruct H; subst. destruct H. inversion H. subst. exists x2. apply eq_refl. split. apply rt_refl. exists v; auto. ded (IHclos_refl_trans1 _ _ H1). clear IHclos_refl_trans1. destruct H2. destruct H3 as [w]. ded (IHclos_refl_trans2 _ _ H3). destruct H4. destruct H5. split. eapply rt_trans; eauto. exists x0. auto. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)