From c8ec0670f8d71dc1e904d1da8c682e60c50551fb Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 30 Oct 2023 12:34:36 +0100 Subject: [PATCH] Update --- src/subsequences.v | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 00c819b..fab3f58 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -314,18 +314,10 @@ Proof. = map snd (filter fst (combine (repeat false (length u)) u))). intro u. induction u. reflexivity. simpl. assumption. apply H0. exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity. - (* deux cas : a = n ou non *) assert ({a=T} + {a<>T}). apply I. destruct H. rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl. - - - - - - destruct H. destruct H. destruct H. - assert (x0 = nil). symmetry in H. apply length_zero_iff_nil in H. - assumption. rewrite H1 in H0. simpl in H0. + rewrite subsequence_cons_eq. split; intro; assumption.