proposition: Lemma term_denote_subst_term env v v' t : term_denote env v = term_denote env v' → term_denote env (subst_term t v v') = term_denote env t.
proof: Proof. unfold subst_term; intros. destruct term_beq eqn:?; auto. apply term_beq_sound in Heqb. congruence. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt