Commit dd191041 authored by Xavier Leroy's avatar Xavier Leroy Committed by Xavier Leroy
Browse files

Add lemma list_norepet_rev

parent e81d015e
......@@ -1011,6 +1011,14 @@ Proof.
generalize list_norepet_app; firstorder.
Qed.
Lemma list_norepet_rev:
forall (A: Type) (l: list A), list_norepet l -> list_norepet (List.rev l).
Proof.
induction 1; simpl.
- constructor.
- apply list_norepet_append_commut. simpl. constructor; auto. rewrite <- List.in_rev; auto.
Qed.
(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
Inductive is_tail (A: Type): list A -> list A -> Prop :=
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment