blob: 9f10f7490e9df34bcec4e4dcd995aaa5e347613a (
plain)
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.
|