-lemma prApp_not_dummy_not_lambda:
-∀M,N,P. pr (App M N) P → is_dummy M = false → is_lambda M = false →
-∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
-#M #N #P #prH (inversion prH)
- [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #_ #H1 destruct
- |#M1 #N1 #P1 #_ #_ #H destruct #_ #H1 destruct
- |#M #N #P1 #_ #_ #H destruct
- |#Q #eqProd #_ #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
- |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ #_ destruct
- @(ex_intro … N1) @(ex_intro … N2) /3/
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
- |#M #N #_ #_ #H destruct
+lemma red_lift: ∀N,N1,n. red N N1 → ∀k. red (lift N k n) (lift N1 k n).
+#N #N1 #n #r1 (elim r1) normalize /2/
+qed.
+
+(* star red *)
+lemma star_appl: ∀M,M1,N. star … red M M1 →
+ star … red (App M N) (App M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_appr: ∀M,N,N1. star … red N N1 →
+ star … red (App M N) (App M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (App M N) (App M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (App M1 N)) /2/
+qed.
+
+lemma star_laml: ∀M,M1,N. star … red M M1 →
+ star … red (Lambda M N) (Lambda M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_lamr: ∀M,N,N1. star … red N N1 →
+ star … red (Lambda M N) (Lambda M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (Lambda M N) (Lambda M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (Lambda M1 N)) /2/
+qed.
+
+lemma star_prodl: ∀M,M1,N. star … red M M1 →
+ star … red (Prod M N) (Prod M1 N).
+#M #M1 #N #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_prodr: ∀M,N,N1. star … red N N1 →
+ star … red (Prod M N) (Prod M N1).
+#M #N #N1 #star1 (elim star1) //
+#B #C #starMB #redBC #H @(inj … H) /2/
+qed.
+
+lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
+ star … red (Prod M N) (Prod M1 N1).
+#M #M1 #N #N1 #redM #redN @(trans_star ??? (Prod M1 N)) /2/
+qed.
+
+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/
+qed.
+
+lemma red_subst1 : ∀M,N,N1,i. red N N1 →
+ (star … red) M[i≝N] M[i≝N1].
+#M (elim M)
+ [//
+ |#i #P #Q #n #r1 (cases (true_or_false (leb i n)))
+ [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
+ [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
+ |#eqin >eqin >subst_rel2 >subst_rel2 @R_to_star /2/
+ ]
+ |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
+ >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
+ ]
+ |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_app /2/
+ |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_lam /2/
+ |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_prod /2/
+ |#P #Hind #M #N #i #r1 normalize @star_d /2/