proposition: Lemma dup_int_subst_spec : forall s t, sub (dup_int_subst s) (dup_int_term t) = dup_int_term (sub s t).
proof: Proof. intros. pattern t. set (Q := Vforall (fun t0 => sub (dup_int_subst s) (dup_int_term t0) = dup_int_term (sub s t0))). apply term_ind with (Q:=Q). intro; unfold dup_int_subst; simpl. apply eq_refl. intros. rewrite dup_int_term_fun. simpl. unfold Q in H. cut (Vmap (sub (dup_int_subst s)) (Vmap dup_int_term v) = Vmap dup_int_term (Vmap (sub s) v)). intros. rewrite <- H0. auto. rewrite !Vmap_map. apply Vmap_eq. apply H. unfold Q; simpl; auto. unfold Q; simpl; auto. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)