- new extendedd beta-reductum involving native type annotation

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
index 35500d952b1f0c343ed6453146756a9b3ca7b381..0c899ad444fca856e47f68de32d0cfcaea081996 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
@@ -90,32 +90,39 @@ let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
            ]
    ].
 
-(* Basic properties *********************************************************)
+(* Basic inversion lemmas ***************************************************)
 
-lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
-#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2  [ <minus_n_O // ]
-#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
-qed.
-
-lemma deg_pred: ∀h,g,k,l. deg h g (next h k) (l + 1) → deg h g k (l + 2).
+lemma deg_inv_pred: ∀h,g,k,l. deg h g (next h k) (l+1) → deg h g k (l+2).
 #h #g #k #l #H1
 elim (deg_total h g k) #l0 #H0
 lapply (deg_next … H0) #H2
 lapply (deg_mono … H1 H2) -H1 -H2 #H
 <(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
-qed.
+qed-.
 
-lemma deg_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
+lemma deg_inv_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
 #h #g #k #l @(nat_ind_plus … l) -l //
 #l #IHl #l0 >iter_SO #H
-lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H
+lapply (deg_inv_pred … H) -H <(associative_plus l0 1 1) #H
 lapply (IHl … H) -IHl -H //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
+#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2  [ <minus_n_O // ]
+#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
 qed.
 
+lemma deg_next_SO: ∀h,g,k,l. deg h g k (l+1) → deg h g (next h k) l.
+#h #g #k #l #Hkl
+lapply (deg_next … Hkl) -Hkl <minus_plus_m_m //
+qed-.
+
 lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
 #h #k #l <plus_n_Sm <plus_n_Sm //
 qed.
 
 lemma sd_l_correct: ∀h,l,k. deg h (sd_l h k l) k l.
-#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1/
+#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1 by deg_inv_pred/
 qed.