5
Inductive liste : Set :=
7
| c : A -> liste -> liste.
9
Inductive e : A -> liste -> Prop :=
10
| ec : forall (x : A) (l : liste), e x (c x l)
11
| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
13
Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.
15
Definition same_refl (x:liste) : (same x x).
16
unfold same; split; intros; trivial.
19
Goal forall (x:liste), (same x x).