proposition: Lemma E_app s t P Q ρ : E (poly_arr s t) ρ P -> E s ρ Q -> E t ρ (app P Q).
proof: Proof. revert P Q. eapply E2_ind. intros P Q nP nQ IHP IHQ. econstructor. inversion 1. intros R Hst. inv Hst; eauto. destruct nP. rewrite K_arr in H; eauto. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms