Update
This commit is contained in:
parent
c9a99e597b
commit
00cf74be9c
@ -217,7 +217,7 @@ Proof.
|
|||||||
simpl. rewrite IHv. rewrite repeat_length. reflexivity.
|
simpl. rewrite IHv. rewrite repeat_length. reflexivity.
|
||||||
inversion I. reflexivity.
|
inversion I. reflexivity.
|
||||||
|
|
||||||
rewrite H1. reflexivity. inversion H. reflexivity. rewrite H0.
|
rewrite H1; inversion H; reflexivity. rewrite H0.
|
||||||
assert (forall (u: list X) v w,
|
assert (forall (u: list X) v w,
|
||||||
filter fst (combine (repeat false (length u) ++ v) (u ++ w))
|
filter fst (combine (repeat false (length u) ++ v) (u ++ w))
|
||||||
= filter fst (combine v w)).
|
= filter fst (combine v w)).
|
||||||
@ -231,9 +231,9 @@ Proof.
|
|||||||
intro v. induction v; intro u; intro I.
|
intro v. induction v; intro u; intro I.
|
||||||
apply length_zero_iff_nil in I. rewrite I. reflexivity.
|
apply length_zero_iff_nil in I. rewrite I. reflexivity.
|
||||||
destruct u. apply O_S in I. contradiction I.
|
destruct u. apply O_S in I. contradiction I.
|
||||||
simpl. rewrite H1. rewrite <- IHv. reflexivity. inversion I.
|
simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
|
||||||
reflexivity. rewrite H1. rewrite <- H2. reflexivity.
|
|
||||||
inversion H. reflexivity.
|
rewrite H1. rewrite <- H2; inversion H; reflexivity.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user