proposition: Lemma subst_extensional sigma tau s: (forall x, x ∈ vars s -> sigma x = tau x) -> sigma • s = tau • s.
proof: Proof. induction s in sigma, tau |-*; eauto. - intros H; cbn; f_equal; eapply IHs. intros [] ?; cbn; eauto. unfold funcomp; rewrite H; eauto. - intros; cbn; erewrite IHs1, IHs2; eauto. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)