Problem:
 all (\x. P) -> P
 all (\x. and (P' x) (Q' x)) -> and (all P') (all Q')
 all (\x. or (P' x) Q) -> or (all P') Q
 all (\x. or P (Q' x)) -> or P (all Q')

Proof:
 Higher-Order Church Rosser Processor:
  all (\x. P) -> P
  all (\x. and (P' x) (Q' x)) -> and (all P') (all Q')
  all (\x. or (P' x) Q) -> or (all P') Q
  all (\x. or P (Q' x)) -> or P (all Q')
  critical peaks: 8
   and 8 9 <-[]-> and (all (\x. 8)) (all (\x. 9))
   or 13 14 <-[]-> or (all (\x. 13)) 14
   or 18 19 <-[]-> or 18 (all (\x. 19))
   and (all (\x. 24)) (all (\x. 25)) <-[]-> and 24 25
   or (all (\x. 44)) 45 <-[]-> or 44 45
   or (all (\x. 59)) 60 <-[]-> or 59 (all (\x. 60))
   or 66 (all (\x. 67)) <-[]-> or 66 67
   or 78 (all (\x. 79)) <-[]-> or (all (\x. 78)) 79
   
   Higher-Order Closedness Processor:
     all critical pairs are (almost) development closed
    
    Qed