proposition: Lemma app_fcap : forall m s, (forall x, x <= m -> s x = Var x) -> forall t, maxvar t <= m -> forall v, sub s (fcap (capa t) v) = fcap (capa t) (Vmap (sub s) v).
proof: Proof. intros until t. pattern t. set (Q := fun n (ts : terms n) => maxvars ts <= m -> forall v, Vmap (sub s) (Vmap_sum (Vmap capa ts) v) = Vmap_sum (Vmap capa ts) (Vmap (sub s) v)). apply term_ind with (Q := Q); clear t. intros. unfold fcap. simpl. apply H. hyp. intros f ts IH H0. simpl. unfold fcap. case (defined f R); simpl; intros. VSntac v. refl. apply args_eq. apply IH. hyp. unfold Q. auto. intros. unfold Q. simpl. intros. gen (Vbreak_eq_app v0). intro. rewrite H3, Vmap_app, !Vbreak_app. simpl. rewrite maxvars_cons in H2. apply Vcons_eq_intro. apply H0. eapply le_max_elim_l. apply H2. apply H1. eapply le_max_elim_r. apply H2. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)