proposition: Lemma sub_comp_single s x (u : term) : s x = sub s u -> forall t, sub (sub_comp s (single x u)) t = sub s t.
proof: Proof. intros. set (s' := sub_comp s (single x u)). pattern t. apply term_ind with (Q := fun n (ts : terms n) => Vmap (sub s') ts = Vmap (sub s) ts); clear t. intro. unfold s', sub_comp, single. simpl. case_beq_nat x x0; auto. intros f v IH. rewrite !sub_fun. f_equal. hyp. refl. intros. simpl. apply Vcons_eq_intro; hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)