Update
This commit is contained in:
parent
49649d6fd0
commit
d62a5752ae
@ -329,10 +329,10 @@ Proof.
|
|||||||
|
|
||||||
|
|
||||||
assert ({a=x} + {a<>x}). apply I. destruct H.
|
assert ({a=x} + {a<>x}). apply I. destruct H.
|
||||||
rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
|
rewrite e. rewrite subsequence3_cons_eq. rewrite <- IHl.
|
||||||
rewrite subsequence_cons_eq. split; intro; assumption.
|
rewrite subsequence_cons_eq. split; intro; assumption.
|
||||||
|
|
||||||
split; intro H. apply subsequence2_cons_l. apply IHl.
|
split; intro H. apply subsequence3_cons_l. apply IHl.
|
||||||
destruct H. destruct H. destruct H.
|
destruct H. destruct H. destruct H.
|
||||||
destruct x0. destruct x1.
|
destruct x0. destruct x1.
|
||||||
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
||||||
@ -342,14 +342,11 @@ Proof.
|
|||||||
reflexivity.
|
reflexivity.
|
||||||
|
|
||||||
apply subsequence_cons_l. apply IHl.
|
apply subsequence_cons_l. apply IHl.
|
||||||
destruct H. destruct H.
|
destruct H. destruct H. destruct H.
|
||||||
destruct x0. simpl in H0.
|
|
||||||
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
destruct x0. inversion H. rewrite H2 in n. contradiction n. reflexivity.
|
||||||
destruct b. simpl in H0. inversion H0. rewrite H2 in n.
|
exists x2. exists x1. split. inversion H. reflexivity. assumption.
|
||||||
contradiction n. reflexivity.
|
Qed.
|
||||||
exists x0. inversion H. inversion H0.
|
|
||||||
split; reflexivity.
|
|
||||||
Admitted.
|
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_dec {X: Type}:
|
Theorem subsequence_dec {X: Type}:
|
||||||
|
Loading…
Reference in New Issue
Block a user