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