proposition: Lemma swap_intro s x y t : ~In y (vars t) -> sub s t = sub (sub_comp s (swap y x)) (sub (swap x y) t).
proof: Proof. pattern t; apply term_ind with (Q := fun n (ts : terms n) => ~In y (vars_vec ts) -> Vmap (sub s) ts = Vmap (sub (sub_comp s (swap y x))) (Vmap (sub (swap x y)) ts)); clear t; intros. simpl. unfold swap, single, sub_comp. case_beq_nat x x0. simpl. rewrite (beq_refl beq_nat_ok). refl. simpl. case_beq_nat y x0. simpl in H. tauto. refl. rewrite !sub_fun, H. refl. rewrite vars_fun in H0. hyp. refl. simpl in *. rewrite in_app in H1. rewrite H0, H. refl. tauto. tauto. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)