proposition: Lemma Vmap_sub_eq s1 s2 n (ts : terms n) : (forall x, In x (vars_vec ts) -> s1 x = s2 x) -> Vmap (sub s1) ts = Vmap (sub s2) ts.
proof: Proof. intro. apply Vmap_eq. apply Vforall_intro. intros. apply sub_eq. intros. apply H. eapply vars_vec_in. apply H1. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)