update in static_2 and basic_2 for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / ntas_nta.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc
new file mode 100644 (file)
index 0000000..3bfa938
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ntas_nta.etc
@@ -0,0 +1,11 @@
+lapply (nta_ntas … H) -H #H
+elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
+[ elim (eq_or_gt n) #H destruct
+  [ <minus_n_O in HU; #HU -Hn
+    /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
+  | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
+    <minus_n_n in HU; #HU
+    @or_intror
+    @(ex6_5_intro … Ha … HUX HX) -Ha -X
+    [2,4: /2 width=2 by ntas_inv_nta/
+    |6: @ntas_refl