Update
This commit is contained in:
parent
e845183004
commit
79f9525fbd
@ -1138,45 +1138,43 @@ Proof.
|
||||
rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.
|
||||
|
||||
destruct b; destruct b0.
|
||||
reflexivity.
|
||||
rewrite count_occ_app in H9. rewrite count_occ_app in H9.
|
||||
rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
|
||||
rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
|
||||
rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
|
||||
rewrite count_occ_app in H5. rewrite count_occ_app in H5.
|
||||
rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
|
||||
rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
|
||||
rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
|
||||
rewrite H5 in H9.
|
||||
rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
|
||||
rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
|
||||
rewrite Nat.add_cancel_l in H9. inversion H9.
|
||||
reflexivity. easy. easy. reflexivity.
|
||||
rewrite count_occ_app in H9. rewrite count_occ_app in H9.
|
||||
rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
|
||||
rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
|
||||
rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
|
||||
rewrite count_occ_app in H5. rewrite count_occ_app in H5.
|
||||
rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
|
||||
rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
|
||||
rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
|
||||
rewrite <- H5 in H9.
|
||||
rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
|
||||
rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
|
||||
rewrite Nat.add_cancel_l in H9. inversion H9.
|
||||
easy. reflexivity. reflexivity. easy.
|
||||
reflexivity.
|
||||
|
||||
rewrite app_assoc_reverse. apply app_inv_head_iff.
|
||||
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
|
||||
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
|
||||
apply app_inv_head_iff. apply app_inv_head_iff.
|
||||
rewrite app_assoc_reverse.
|
||||
apply app_inv_head_iff. apply app_inv_head_iff.
|
||||
rewrite app_assoc_reverse.
|
||||
reflexivity.
|
||||
|
||||
reflexivity.
|
||||
+ reflexivity.
|
||||
+ rewrite count_occ_app in H9. rewrite count_occ_app in H9.
|
||||
rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
|
||||
rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
|
||||
rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
|
||||
rewrite count_occ_app in H5. rewrite count_occ_app in H5.
|
||||
rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
|
||||
rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
|
||||
rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
|
||||
rewrite H5 in H9.
|
||||
rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
|
||||
rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
|
||||
rewrite Nat.add_cancel_l in H9. inversion H9.
|
||||
reflexivity. easy. easy. reflexivity.
|
||||
+ rewrite count_occ_app in H9. rewrite count_occ_app in H9.
|
||||
rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
|
||||
rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
|
||||
rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
|
||||
rewrite count_occ_app in H5. rewrite count_occ_app in H5.
|
||||
rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
|
||||
rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
|
||||
rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
|
||||
rewrite <- H5 in H9.
|
||||
rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
|
||||
rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
|
||||
rewrite Nat.add_cancel_l in H9. inversion H9.
|
||||
easy. reflexivity. reflexivity. easy.
|
||||
+ reflexivity.
|
||||
+ rewrite app_assoc_reverse. apply app_inv_head_iff.
|
||||
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
|
||||
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
|
||||
apply app_inv_head_iff. apply app_inv_head_iff.
|
||||
rewrite app_assoc_reverse.
|
||||
apply app_inv_head_iff. apply app_inv_head_iff.
|
||||
rewrite app_assoc_reverse.
|
||||
reflexivity.
|
||||
+ reflexivity.
|
||||
Qed.
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user