aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/38.v
blob: 4fc8d7c97dd6cc21d9d3369c49e914255052bc2e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
Require Import Setoid.

Variable A : Set.

Inductive liste : Set :=
| vide : liste
| c : A -> liste -> liste.

Inductive e : A -> liste -> Prop :=
| ec : forall (x : A) (l : liste), e x (c x l)
| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).

Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.

Definition same_refl (x:liste) : (same x x).
  unfold same; split; intros; trivial.
Save.

Goal forall (x:liste), (same x x).
  intro.
  apply (same_refl x).
Qed.