-lemma d2_deliftable_sn_llstar: ∀R. d_deliftable2_sn R →
- ∀d. d_deliftable2_sn (llstar … R d).
-#R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
+lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R →
+ ∀d. d_deliftable2_sn C S (llstar … R d).
+#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2