- some renaming according to the written version of basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / da_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma
index dccb10f9bc70651bda04bb03c4e77e60c335d9eb..c7903c24e4ba51dce66458f52c8e2860d2e900fa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma
@@ -12,13 +12,20 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/static/da_sta.ma".
-include "basic_2/static/sta_aaa.ma".
+include "basic_2/static/aaa_lift.ma".
+include "basic_2/static/da.ma".
 
 (* DEGREE ASSIGNMENT FOR TERMS **********************************************)
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma aaa_da: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l.
-#h #g #G #L #T #A #H elim (aaa_sta h … H) -A /2 width=2 by sta_da/
+lemma aaa_da: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∃d. ⦃G, L⦄ ⊢ T ▪[h, g] d.
+#h #g #G #L #T #A #H elim H -G -L -T -A
+[ #G #L #k elim (deg_total h g k) /3 width=2 by da_sort, ex_intro/
+| * #G #L #K #V #B #i #HLK #_ * /3 width=5 by da_ldef, da_ldec, ex_intro/
+| #a #G #L #V #T #B #A #_ #_ #_ * /3 width=2 by da_bind, ex_intro/
+| #a #G #L #V #T #B #A #_ #_ #_ * /3 width=2 by da_bind, ex_intro/
+| #G #L #V #T #B #A #_ #_ #_ * /3 width=2 by da_flat, ex_intro/
+| #G #L #W #T #A #_ #_ #_ * /3 width=2 by da_flat, ex_intro/
+]
 qed-.