proposition: Lemma rtc_red_dup_int_hd_symb_aux : forall f u v, red R' # u v -> forall us, u = Fun' (hd_symb f) us -> exists vs, v = Fun' (hd_symb f) vs.
proof: Proof. induction 1; intros. eapply red_dup_int_hd_symb. subst. apply H. eauto. destruct (IHclos_refl_trans1 _ H1). eapply IHclos_refl_trans2. apply H2. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)