(* -------------------------------------------------------------------------- *)
ntheorem prove_birds_are_compatible_1:
(* -------------------------------------------------------------------------- *)
ntheorem prove_birds_are_compatible_1:
∀a: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)).
∀a: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)).