proposition: Lemma consts_subst_in x sigma s: x ∈ consts (sigma • s) -> x ∈ consts s \/ exists y, y ∈ vars s /\ x ∈ consts (sigma y).
proof: Proof. induction s in sigma |-*. - right; exists f; intuition. - cbn; intuition. - intros H % IHs; cbn -[vars]; intuition idtac. destruct H0 as [[]]; cbn -[vars] in *; intuition idtac. right. exists n. intuition eauto with listdb. unfold funcomp in H1; now rewrite consts_ren in H1. - cbn; simplify; intuition idtac. + specialize (IHs1 _ H0); intuition idtac. destruct H as [y]; right; exists y; intuition (auto with datatypes). + specialize (IHs2 _ H0); intuition idtac. destruct H as [y]; right; exists y; intuition (auto with datatypes). Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)