-lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
- ∀l. deliftable_sn (lstar S … R l).
-#S #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
-#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
-elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
-elim (IHN2 … HMN) -N /3 width=3/
+lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
+ ∀l. sdeliftable_sn (lstar S … R l).
+#S #R #HR #l #h #G1 #G2 #H
+@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
+#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
+elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
+elim (IHG2 … HFG) -G /3 width=3/