(* ---- FAx -[response(x,x) = x]. *)
ntheorem prove_the_bird_exists:
(* ---- FAx -[response(x,x) = x]. *)
ntheorem prove_the_bird_exists:
∀compose:∀_:Univ.∀_:Univ.Univ.
∀mocking_bird:Univ.
∀response:∀_:Univ.∀_:Univ.Univ.
∀H0:∀W:Univ.∀X:Univ.∀Y:Univ.eq Univ (response (compose X Y) W) (response X (response Y W)).
∀compose:∀_:Univ.∀_:Univ.Univ.
∀mocking_bird:Univ.
∀response:∀_:Univ.∀_:Univ.Univ.
∀H0:∀W:Univ.∀X:Univ.∀Y:Univ.eq Univ (response (compose X Y) W) (response X (response Y W)).