proposition: Lemma lab_fval : forall v t n, n > maxvar t -> lab (fval v n) t = lab v t.
proof: Proof. intros v t. pattern t; apply term_ind with (Q := fun n (ts : terms n) => forall n, n > maxvars ts -> Vmap (lab v) ts = Vmap (lab (fval v n)) ts); clear t; simpl; intros. refl. rewrite (H n). assert (Vmap (int v) v0 = Vmap (int (fval v n)) v0). apply Vmap_eq. apply Vforall_intro. intros. apply term_int_eq_fval_lt. apply Nat.le_lt_trans with (Vmax (Vmap (@maxvar Sig) v0)). apply Vmax_in. apply Vin_map_intro. hyp. hyp. rewrite H1. refl. unfold maxvars. lia. refl. rewrite maxvars_cons, gt_max in H1. destruct H1. rewrite (H0 n0). 2: hyp. rewrite (H n0). 2: hyp. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)