proposition: Lemma select_variables_subst X S I sigma: I ⊆ nats (length S) -> map (subst_exp (S .+ sigma)) (map (@var_exp X) I) = select I S.
proof: Proof. intros. rewrite map_map; cbn. induction I; cbn; eauto. destruct (nth_error S a) eqn: H1. + rewrite IHI; firstorder. f_equal. now eapply nth_error_sapp. + exfalso. apply nth_error_None in H1. specialize (H a). mp H; [now left|]. eapply nats_lt in H. lia. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)