proposition: Lemma head_subst (s: exp X) sigma: (forall x, ~ isApp (sigma x)) -> sigma • (head s) = head (sigma • s).
proof: Proof. intros H; induction s. - cbn; specialize (H f). destruct (sigma f); cbn in *; intuition. - reflexivity. - reflexivity. - cbn; congruence. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)