proposition: Lemma hd_red_dup_hd_red : forall t u, hd_red R t u -> hd_red (dup_hd_rules R) (dup_hd_term t) (dup_hd_term u).
proof: Proof. intros. redtac. subst. unfold hd_red. ex (dup_hd_term l) (dup_hd_term r) (dup_int_subst s). ded (is_notvar_lhs_elim hyp lr). decomp H. ded (is_notvar_rhs_elim hyp' lr). decomp H. subst. rewrite !dup_int_subst_hd_dup. split_all. unfold dup_hd_rules. change (In (dup_hd_rule (mkRule (Fun x x0) (Fun x1 x2))) (map dup_hd_rule R)). apply in_map. hyp. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)