fact: Fixpoint Kleene_assoc {I O} (F : I ▷ O) (p q r : I → Type) (f : p :→ F :* q) (g : q :→ F :* r) (i : I) (m : (F :* p) i) : Kleene_extend F g i (Kleene_extend F f i m) = Kleene_extend F (λ (x : I) (a : p x), Kleene_extend F g x (f x a)) i m.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple