proposition: Lemma compat_app A B s t: E (A → B) s -> E A t -> E B (s t).
proof: Proof. intros (v1 & [H1 H2] & H3). intros (v2 & [H4 H5] & H6). eapply closure_under_reduction. rewrite H1, H4; eauto. destruct v1. 1, 2, 4: eexists; split; [split|]; eauto; cbn; intuition. cbn in H3; mp H3; cbn; intuition. specialize (H0 v2 id); asimpl in H0; unfold id in H0. eapply H0; exists v2; split; [split|]; eauto. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)