proposition: Lemma Ft_epi : forall v t, unlab (lab v t) = t.
proof: Proof. intros v t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => Vmap (unlab o lab v) ts = ts); clear t; intros; simpl. refl. apply args_eq. unfold comp in H. rewrite Vmap_map, H. apply Vcast_refl. refl. rewrite H0. unfold comp. rewrite H. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)