proposition: Lemma sapp_lt_in X x (A: list X) sigma: x < length A -> (A .+ sigma) x ∈ A.
proof: Proof. intros H. eapply nth_error_In with (n := x). eapply nth_error_lt_Some in H as [a]. erewrite nth_error_sapp; eauto. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)