+lemma SN_DAPP: ∀N,M. SN (App M N) → SN (App (D M) N).
+cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/]
+#P #snP (elim snP) #Q #snQ #Hind
+#M #N #eqQ % #A #rA (cases (red_app … rA))
+ [*
+ [*
+ [* #M1 * #N1 * #eqH destruct
+ |* #M1 * #eqH destruct #eqA >eqA @SN_d % @snQ
+ ]
+ |* #M1 * #eqA #red1 (cases (red_d …red1))
+ #M2 * #eqM1 #r2 >eqA >eqM1 @(Hind (App M2 N)) /2/
+ ]
+ |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/
+ ]
+qed.
+
+lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M.