proposition: Lemma compA {a b c d : Type} (h : a -> b) (g : b -> c) (f : c -> d) : (f \o g) \o h = f \o (g \o h).
proof: Proof. reflexivity. Qed.
imports: Hask.Ltac Hask.Data.Either Hask.Data.Maybe Hask.Data.Tuple Hask.Data.Functor Coq.micromega.Lia