test-suite/bugs/closed/shouldsucceed/1568.v


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

CoInductive A: Set :=
  mk_A: B -> A
with B: Set :=
  mk_B: A -> B.

CoFixpoint a:A := mk_A b
with b:B := mk_B a.

Goal b = match a with mk_A a1 => a1 end.
  simpl. reflexivity.
Qed.