-∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f (f B (f B (f (f C C) A))) A) C))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b))))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f (f B (f B (f (f C C) A))) A) C))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b)))))