test-suite/bugs/closed/4433.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

Require Import Coq.Arith.Arith Coq.Init.Wf.
Axiom proof_admitted : False.
Goal exists x y z : nat, Fix
                           Wf_nat.lt_wf
                           (fun _ => nat -> nat)
                           (fun x' f => match x' as x'0
                                              return match x'0 with
                                                       | 0 => True
                                                       | S x'' => x'' < x'
                                                     end
                                                     -> nat -> nat
                                        with
                                          | 0 => fun _ _ => 0
                                          | S x'' => f x''
                                        end
                                          (match x' with
                                             | 0 => I
                                             | S x'' => (Nat.lt_succ_diag_r _)
                                           end))
                           z
                           y
                         = 0.
Proof.
  do 3 (eexists; [ shelve.. | ]).
  match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end.
  case proof_admitted.
  Unshelve.
  all:constructor.
Defined.