proposition: Lemma red_dup_int_red : forall t u, red R t u -> red (dup_int_rules R) (dup_int_term t) (dup_int_term u).
proof: Proof. intros. redtac. exists (dup_int_term l). exists (dup_int_term r). exists (dup_int_context c). exists (dup_int_subst s). split. change (In (dup_int_rule (mkRule l r)) (map dup_int_rule R)). apply in_map. auto. rewrite <- !dup_int_context_spec. split; subst; refl. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)