proposition: Lemma asimpl_f_atom P v s : (atom P v)[s] = atom P (Vector.map (subst_term s) v).
proof: Proof. easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid