test-suite/output/bug_13266.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

Inductive proc : Type -> Type :=
| Tick : proc unit
.

Inductive exec :
  forall T, proc T -> T -> Prop :=
| ExecTick :
    exec _ (Tick) tt
.

Lemma foo :
  exec _ Tick tt ->
  True.
Proof.
  intros H. 
  remember Tick as p.
  Fail induction H.
Abort.