baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-11-01 21:08:36 +01:00
parent 24d88f1928
commit 43d97734b2
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/subsequences.v
View File

@ -425,9 +425,8 @@ Proof.
apply length_zero_iff_nil in I. rewrite I. reflexivity.
destruct u0. reflexivity. destruct v0.
apply PeanoNat.Nat.neq_succ_0 in J; contradiction J.
destruct b; simpl; rewrite K; rewrite IHw.
reflexivity. inversion I; reflexivity. inversion J; reflexivity.
reflexivity. inversion I; reflexivity. inversion J; reflexivity.
destruct b; simpl; rewrite K; rewrite IHw;
inversion I; inversion J; reflexivity.
rewrite H4; try rewrite H1; try rewrite H; reflexivity.
Qed.