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 19:13:41 +01:00
parent 995a822cae
commit bc25f2d521
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/subsequences.v
View File

@ -311,7 +311,7 @@ Proof.
assert ({ subsequence2 l s } + { ~ subsequence2 l s }). assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
apply subsequence2_dec. assumption. destruct H0. apply subsequence2_dec. assumption. destruct H0.
apply subsequence_eq_def_2 in s0. left. assumption. apply subsequence_eq_def_2 in s0. left. assumption.
right. unfold not. intro I. right. intro I.
apply subsequence_eq_def_3 in I. apply subsequence_eq_def_3 in I.
apply subsequence_eq_def_1 in I. apply subsequence_eq_def_1 in I.
apply n in I. contradiction I. apply n in I. contradiction I.
@ -326,7 +326,7 @@ Proof.
assert ({ subsequence3 l s } + { ~ subsequence3 l s }). assert ({ subsequence3 l s } + { ~ subsequence3 l s }).
apply subsequence3_dec. assumption. destruct H0. apply subsequence3_dec. assumption. destruct H0.
apply subsequence_eq_def_3 in s0. left. assumption. apply subsequence_eq_def_3 in s0. left. assumption.
right. unfold not. intro I. right. intro I.
apply subsequence_eq_def_1 in I. apply subsequence_eq_def_1 in I.
apply subsequence_eq_def_2 in I. apply subsequence_eq_def_2 in I.
apply n in I. contradiction I. apply n in I. contradiction I.