proposition: Lemma dup_int_rules_int_red_rtc : forall f v t, red R # (Fun' (hd_symb f) v) t -> int_red R # (Fun' (hd_symb f) v) t.
proof: Proof. intros. ded (dup_int_rules_int_red_rtc_aux H (eq_refl _)). tauto. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)