-∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f C A)) D) (f A (f (f (f (f (f (f B B) A) C) C) A) B))) 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 C A)) D) (f A (f (f (f (f (f (f B B) A) C) C) A) B))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b)))))