proposition: Lemma lab_sub_eq : forall v s t, lab v (sub s t) = sub (lab_sub v s) (lab (beta v s) t).
proof: Proof. intros v s t. pattern t; apply term_ind with (Q := fun n (ts : terms n) => Vmap (lab v o sub s) ts = Vmap (sub (lab_sub v s) o lab (beta v s)) ts); clear t; intros; simpl. unfold lab_sub. refl. rewrite !Vmap_map, Vmap_eq_ext with (g := int (beta v s)). 2: apply substitution_lemma. apply args_eq. hyp. refl. apply Vcons_eq_intro; hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)