fact: Definition schainl_aux (n : nat) (rec : Box LChain n) : LChain n := fun sa op => Category.bind (runParser (call op (small sa)) (Nat.le_refl _) (leftovers sa)) (fun sop => let sa' := Success.map (fun f => f (value sa)) sop in Category.bind (call rec (small sa) sa' (Induction.lt_lower (small sa) op)) (fun res => pure (lt_lift (small sa) res))).
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)