The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I was looking at proving monad properties of:

CoInductive Coroutine (X:Type) : Type :=
| coroutine_return : X -> Coroutine X
| yield_with_continuation : Coroutine X -> Coroutine X.

Implicit Arguments coroutine_return [[X]].
Implicit Arguments yield_with_continuation [[X]].

I was eventually able to prove the necessary identities, assuming the axiom:

CoInductive coroutine_eq {X} : Coroutine X -> Coroutine X -> Prop :=
| coroutine_return_eq: forall x0:X,
    coroutine_eq (coroutine_return x0) (coroutine_return x0)
| yield_eq: forall x y:Coroutine X, coroutine_eq x y ->
    coroutine_eq (yield_with_continuation x) (yield_with_continuation y).
Axiom coroutine_eq_eq: forall {X} (x y:Coroutine X),
  coroutine_eq x y -> x = y.

My question is: is there any way to prove that axiom?  Maybe using a single 
axiom which would also imply corresponding statements for Stream, 
PossiblyTerminatingStream, InfinitelyBranchingBinaryTree, etc.?
-- 
Daniel Schepler