proposition: Lemma sub_extend_notin s x v u : ~In x (vars u) -> sub (extend s x v) u = sub s u.
proof: Proof. set (s' := extend s x v). pattern u. apply term_ind with (Q := fun n (us : terms n) => ~In x (vars_vec us) -> Vmap (sub s') us = Vmap (sub s) us); clear u. intro. simpl. split_all. unfold s', extend. case_beq_nat x0 x; congruence. intros f us. rewrite vars_fun. simpl. intros. apply args_eq. auto. refl. intros u n us. simpl. rewrite in_app. split_all. apply Vcons_eq_intro; intuition. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)