proposition: Lemma sapp_ge_in X x (A: list X) sigma: length A <= x -> sapp A sigma x = sigma (x - length A).
proof: Proof. induction A in x |-*. - cbn. intros _. destruct x; reflexivity. - intros H. destruct x. inv H. cbn; rewrite <-IHA; eauto using le_S_n. Qed.
imports: List Arith Lia Morphisms Undecidability.HOU(calculus.terms)