Minimal language CFA problem. Unary untyped lambda calculus. Can you get this is always true?

mini-church.sch

;; multiplication distributes over addition test: (2 * (1 + 3)) = ((2 * 1) + (2 * 3))
((lambda (plus)
   ((lambda (mult)
      ((lambda (pred)
         ((lambda (sub)
            ((lambda (church0)
               ((lambda (church1)
                  ((lambda (church2)
                     ((lambda (church3)
                        ((lambda (true)
                           ((lambda (false)
                              ((lambda (church0?)
                                 ((lambda (Y)
                                    ((lambda (church=?)
                                       ((church=? ((mult church2) ((plus church1) church3)))
                                        ((plus ((mult church2) church1)) ((mult church2) church3))))
                                     (Y
                                      (lambda (church=?)
                                        (lambda (e1)
                                          (lambda (e2)
                                            (((church0? e1) ;; IF
                                              (lambda (thendummy) (church0? e2)))
                                             (lambda (elsedummy1)
                                               (((church0? e2) ;; IF
                                                 false)
                                                (lambda (elsedummy2) ((church=? ((sub e1) church1)) ((sub e2) church1))))))))))))
                                  (lambda (yf)
                                    ((lambda (yg) (yg yg))
                                     (lambda (yx) (yf (λ (yv) ((yx yx) yv))))))))
                               (lambda (z) ((z (lambda (zx) false)) true))))
                            (lambda (fa) (lambda (fb) (fb (lambda (bdummy) bdummy))))))
                         (lambda (ta) (lambda (tb) (ta (lambda (adummy) adummy))))))
                      (lambda (f3) (lambda (x3) (f3 (f3 (f3 x3)))))))
                   (lambda (f2) (lambda (x2) (f2 (f2 x2))))))
                (lambda (f1) (lambda (x1) (f1 x1)))))
             (lambda (f0) (lambda (x0) x0))))
          (lambda (s1)
            (lambda (s2)
              ((s2 pred) s1)))))
       (lambda (n)
         (lambda (rf)
           (lambda (rx)
             (((n (lambda (g) (lambda (h) (h (g rf)))))
               (lambda (ignored) rx))
              (lambda (id) id)))))))
    (lambda (m1)
      (lambda (m2)
        (lambda (mf) (m2 (m1 mf)))))))
 (lambda (p1)
   (lambda (p2)
     (lambda (pf)
       (lambda (x) ((p1 pf) ((p2 pf) x)))))))