matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc

   1 lapply (nta_ntas … H) -H #H
   2 elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
   3 [ elim (eq_or_gt n) #H destruct
   4   [ <minus_n_O in HU; #HU -Hn
   5     /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
   6   | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
   7     <minus_n_n in HU; #HU
   8     @or_intror
   9     @(ex6_5_intro … Ha … HUX HX) -Ha -X
  10     [2,4: /2 width=2 by ntas_inv_nta/
  11     |6: @ntas_refl