Program.v

Require Import Coq.Program.Tactics.

Program Definition g: {holds: bool | (holds = true)} := true.

Program Definition invoke2 (b: bool) (H: (match b with
                                          | true => g
                                          | false => true
                                          end = true)) : bool := true.