proposition: Lemma rtc_red_dup_int_hd_symb : forall f us v, red R' # (Fun' (hd_symb f) us) v -> exists vs, v = Fun' (hd_symb f) vs.
proof: Proof. intros. eapply rtc_red_dup_int_hd_symb_aux. apply H. refl. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)