-lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
- lstar B R (l+1) b1 b2.
-#B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
-qed.
+lemma lstar_inv_S_dx: ∀B,R,l,b1,b2. lstar B R (l+1) b1 b2 →
+ ∃∃b. lstar B R l b1 b & R b b2.
+#B #R #l #b1 #b2 #H
+elim (lstar_inv_ltransitive B R … H) -H #b #Hb1 #H
+lapply (lstar_inv_step B R … H) -H /2 width=3/
+qed-.