From bf9517f266e6715b7b2a570c51a0167909ae830c Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Mon, 4 Dec 2023 12:03:51 +0100
Subject: [PATCH] Update

---
 src/mapping.v | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/src/mapping.v b/src/mapping.v
index 2239026..48a53ca 100644
--- a/src/mapping.v
+++ b/src/mapping.v
@@ -362,7 +362,8 @@ Proof.
   rewrite seq_length. assumption. rewrite H6. rewrite seq_nth.
   reflexivity. apply Nat.lt_succ_diag_r.
 
-  assert (N: In a (a::s)). apply in_eq. apply K in N.
+  assert (N: In a (a::s)). apply in_eq. apply K in N. assert (M := N).
+  apply H5 in N. destruct N.
 
   rewrite nth_error_nth' with (d := x).
   replace (nth_error (map (fun e : nat => nth (g e) base x)
@@ -376,17 +377,30 @@ Proof.
     -> n < m -> g' (nth (f' n) (seq 0 m) 0) = n).
   intros m n f' g'. intros J J1 J2 J3.
 
-  rewrite H6. apply J2 in J3. destruct J3. apply H7. apply J. assumption.
+  rewrite H6. apply J2 in J3. destruct J3. apply H9. apply J. assumption.
 
-  rewrite H6. apply H5 in N. destruct N. rewrite H8. reflexivity.
-  apply H2. assumption. rewrite H6. apply H5 in N. destruct N.
+  rewrite H6. rewrite H7. reflexivity. apply H2. assumption. rewrite H6.
 
   symmetry. rewrite map_nth_error with (d := f a). reflexivity.
 
   rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity.
+  apply H2. assumption. rewrite seq_length. apply H2. assumption.
+  apply H2. assumption. assumption. intro y. intro G. apply K.
+  apply in_cons. assumption.
 
+  replace (map (fun e : nat => nth e base x) (map g (seq 0 (length base))))
+  with (map (fun z => (fun e => nth e base x) (g z)) (seq 0 (length base))).
+  apply H6.
 
+  assert (forall w (u v: list X),
+    map Some u = map (nth_error v) w -> (forall y, In y w -> y < length v)).
+  intro w; induction w; intros u0 v0; intro J; intro y; intro J1.
+  contradiction. destruct u0. inversion J.
 
+  apply in_inv in J1. destruct J1. rewrite <- H7.
+  inversion J. apply nth_error_Some. rewrite <- H9. easy.
+  apply IHw with (u := u0). inversion J. reflexivity. assumption.
+  apply H7 with (u := x::u). assumption.