fact: Fixpoint eval (rho : env) (t : term) : domain := match t with | var s => rho s | func f v => i_func (Vector.map (eval rho) v) end.
imports: Undecidability.FOL.Syntax.Core Undecidability.FOL.Syntax.Theories Undecidability(Shared.ListAutomation) Vector