matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma

   1 (*
   2 (* Advanced forvard lemmas **************************************************)
   3
   4 lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
   5                      ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
   6 /2 width=3/ qed-.
   7
   8 *)