proposition: Lemma dup_int_subst_hd_dup : forall s f v, sub (dup_int_subst s) (dup_hd_term (Fun f v)) = dup_hd_term (sub s (Fun f v)).
proof: Proof. intros. rewrite dup_hd_term_fun. simpl. cut ((Vmap (sub (dup_int_subst s)) (Vmap dup_int_term v)) = (Vmap dup_int_term (Vmap (sub s) v)) ). intro. rewrite <- H. apply eq_refl. rewrite !Vmap_map. apply Vmap_eq_ext. apply dup_int_subst_spec. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)