proposition: Lemma min_embed_eval' (rho : nat -> V) (t : term') : eval rho (embed_t' t) = eval rho t.
proof: Proof. destruct t as [|[]]. reflexivity. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts ZF FST) Undecidability.FOL.Sets(Models.Aczel Models.ZF_model ZF minZF FST) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_ZFeq PCPb_to_minZF PCPb_to_minZFeq PCPb_to_ZFD) Lia Undecidability.PCP(PCP) Undecidability(Shared.ListAutomation)