X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=541dc6f1200ad8bcb54ea45713a3897af76f7d9c;hp=53e37537cd009ec46e96bdca00f01cb0463a39c7;hb=18a60d7a8ae87aa64c73f9ac03c785b12f8bd25a;hpb=75ce56c45548a1bf66e2a57bfae4186e45d900c7

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