+Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
+
+Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
+ intro il.
+ inversion il.
+ subst.
+ apply X.
+ Defined.
+
+Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
+ intro il.
+ inversion il.
+ subst.
+ apply X0.
+ Defined.
+
+Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
+ induction il; intros; auto.
+ apply INil.
+ inversion X; subst.
+ apply ICons; auto.
+ Defined.
+
+Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
+ induction l1; auto.
+ apply INil.
+ apply ICons.
+ inversion v; auto.
+ apply IHl1.
+ inversion v; auto.
+ Defined.
+
+Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
+ induction l1; auto.
+ apply IHl1.
+ inversion v; subst; auto.
+ Defined.
+
+Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
+ match il with
+ | INil => nil
+ | a::::b => a::(ilist_to_list b)
+ end.
+