-lemma star_d: ∀M,M1. star … red M M1 →
- star … red (D M) (D M1).
-#M #M1 #redM (elim redM) // #B #C #starMB #redBC #H @(inj … H) /2/
+lemma star_dl: ∀M,M1,N. star … red M M1 →
+ star … red (D M N) (D M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_dr: ∀M,N,N1. star … red N N1 →
+ star … red (D M N) (D M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_d: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (D M N) (D M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (D M1 N)) /2/