test-suite/failure/Case2.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Inductive IFExpr : Set :=
  | Var : nat -> IFExpr
  | Tr : IFExpr
  | Fa : IFExpr
  | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.

Type
  (fun F : IFExpr =>
   match F return Prop with
   | IfE (Var _) H I => True
   | IfE _ _ _ => False
   | _ => True
   end).