proposition: Lemma compat_lambda A B s: E B s -> (forall t delta, E A t -> E B (ren delta (lambda s) t)) -> E (A → B) (lambda s).
proof: Proof. intros [t [[H1 H2] _]] ?; cbn; exists (lambda t); intuition; split; rewrite ?H1; eauto. intros; eapply closure_under_expansion; [|eauto]; now rewrite H1. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)