apply IHl1; auto.
Defined.
+Definition ilist_ins {T}{F}{l:list T} z (fz:F z) : forall n (il:IList T F l), IList T F (list_ins n z l).
+ induction l; simpl.
+ intros.
+ destruct n; simpl.
+ apply ICons; [ apply fz | apply INil ].
+ apply ICons; [ apply fz | apply INil ].
+ intros.
+ destruct n; simpl.
+ apply ICons; auto.
+ inversion il; subst.
+ apply ICons; auto.
+ Defined.
+
Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
match il with
| INil => nil
Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
Definition addErrorMessage s {T} (x:OrError T) :=
- x >>=[ s ] (fun y => OK y).
+ x >>=[ eol +++ eol +++ s ] (fun y => OK y).
Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
| Indexed_Error : forall error_message:string, Indexed f (Error error_message)