(* -------------------------------------------------------------------------- *)
ntheorem prove_birds_are_compatible_2:
(* -------------------------------------------------------------------------- *)
ntheorem prove_birds_are_compatible_2:
∀b:Univ.
∀compose:∀_:Univ.∀_:Univ.Univ.
∀mocking_bird:Univ.
∀response:∀_:Univ.∀_:Univ.Univ.
∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (response (compose A B) C) (response A (response B C)).
∀b:Univ.
∀compose:∀_:Univ.∀_:Univ.Univ.
∀mocking_bird:Univ.
∀response:∀_:Univ.∀_:Univ.Univ.
∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (response (compose A B) C) (response A (response B C)).