aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case7.v
blob: f95598aadbef54737a2cd9641b01342770857116 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Inductive List (A : Set) : Set :=
  | Nil : List A
  | Cons : A -> List A -> List A.

Inductive Empty (A : Set) : List A -> Prop :=
    intro_Empty : Empty A (Nil A).

Parameter
  inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x).


Type
  (fun (A : Set) (l : List A) =>
   match l return (Empty A l \/ ~ Empty A l) with
   | Nil _ => or_introl (~ Empty A (Nil A)) (intro_Empty A)
   | Cons _ a y as b => or_intror (Empty A b) (inv_Empty A a y)
   end).