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-23 16:32:28 +01:00
parent 2315f2321e
commit 3e92621520
1 changed files with 0 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/subsequences.v
View File

@ -726,15 +726,6 @@ Theorem subsequence_filter_2 {X: Type} :
forall (u v: list X) f,
subsequence u v -> subsequence (filter f u) (filter f v).
Proof.
(*
intro u. induction u; intros v f; intro H.
assert (v = nil). destruct v. reflexivity.
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
destruct H. destruct H. destruct H.
destruct x0; apply nil_cons in H; contradiction.
rewrite H0. apply subsequence_nil_r.
simpl. destruct (f a).
*)
intros u v. generalize u. induction v; intros u0 f; intro H.
apply subsequence_nil_r.