proposition: Lemma asimpl_t_func t v s : (func t v)`[s] = (func t (Vector.map (subst_term s) v)).
proof: Proof. reflexivity. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid