ndefinition associative: ∀A:Type[0].∀f:A→A→A.Prop
≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
+(*
ntheorem eq_f_g_h:
∀A,B,C,D:Type[0].∀f:C→D.∀g:B→C.∀h:A→B.
f∘(g∘h) = (f∘g)∘h.
//.
-nqed.
+nqed. *)
(* functions and relations *)
ndefinition monotonic : ∀A:Type.∀R:A→A→Prop.