proposition: Lemma term_denote_substitution {env t0 t1 t2 t3} : substitution t0 t1 = Some (t2, t3) → term_denote env t0 = term_denote env t1 → term_denote env t2 = term_denote env t3.
proof: Proof. intros. destruct t0, t1; simpl in H; try (destruct (Pos.eq_dec _ _); [discriminate|]); now inversion_clear H. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt