proposition: Lemma int_red_dup_int_red : forall t u, int_red R t u -> red (dup_int_rules R) (dup_hd_term t) (dup_hd_term u).
proof: Proof. intros. redtac. ex (dup_int_term l) (dup_int_term r) (dup_hd_context c) (dup_int_subst s). destruct c. tauto. split. change (In (dup_int_rule (mkRule l r)) (map dup_int_rule R)). apply in_map. auto. subst; simpl. split; rewrite Vmap_cast, Vmap_app; simpl; rewrite <- dup_int_context_spec; auto. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)