1
Inductive List (A : Set) : Set :=
3
| Cons : A -> List A -> List A.
5
Inductive eqlong : List nat -> List nat -> Prop :=
7
forall (n m : nat) (x y : List nat),
8
eqlong x y -> eqlong (Cons nat n x) (Cons nat m y)
9
| eql_nil : eqlong (Nil nat) (Nil nat).
12
Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat).
15
forall (a : nat) (x : List nat),
16
eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x).
19
forall (a : nat) (x : List nat),
20
eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat).
23
forall (a : nat) (x : List nat) (b : nat) (y : List nat),
24
eqlong (Cons nat a x) (Cons nat b y) \/
25
~ eqlong (Cons nat a x) (Cons nat b y).
29
forall (n m : nat) (x y : List nat),
30
~ eqlong x y -> ~ eqlong (Cons nat n x) (Cons nat m y).
32
inv_r : forall (n : nat) (x : List nat), ~ eqlong (Nil nat) (Cons nat n x).
34
inv_l : forall (n : nat) (x : List nat), ~ eqlong (Cons nat n x) (Nil nat).
36
Fixpoint eqlongdec (x y : List nat) {struct x} :
37
eqlong x y \/ ~ eqlong x y :=
38
match x, y return (eqlong x y \/ ~ eqlong x y) with
39
| Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
40
| Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
41
| Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x)
42
| Cons a x as L1, Cons b y as L2 =>
43
match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
44
| or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
45
| or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
51
match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
52
| Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
53
| Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
54
| Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x)
55
| Cons a x as L1, Cons b y as L2 =>
56
match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
57
| or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
58
| or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)