From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 11 Jul 2011 05:04:16 +0000 (-0700)
Subject: General: add ilist_ins
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=18a60d7a8ae87aa64c73f9ac03c785b12f8bd25a

General: add ilist_ins
---

diff --git a/src/General.v b/src/General.v
index 53e3753..541dc6f 100644
--- a/src/General.v
+++ b/src/General.v
@@ -912,6 +912,19 @@ Lemma ilist_app {T}{F}{l1:list T}(v1:IList T F l1) : forall {l2:list T}(v2:IList
   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