proposition: Lemma substitution_lemma xint s t : term_int xint (sub s t) = term_int (beta xint s) t.
proof: Proof. pattern t; eapply term_ind with (Q := fun n (ts : terms n) => Vmap (term_int xint) (Vmap (sub s) ts) = Vmap (term_int (beta xint s)) ts). intro x. simpl. refl. intros f ts. simpl. intro H. f_equal. hyp. simpl. refl. intros. simpl. rewrite H, <- H0. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)