decide equality for Mutually Recursive Types in Coq?

Question

Is there any way to use the decide equality tactic with mutually recursive types in Coq?

For example, if I've got something like this:

Inductive LTree : Set :=
| LNil
| LNode (x: LTree) (y: RTree)
with RTree : Set :=
| RNil
| RNode (x: LTree) (y: RTree).

Lemma eq_LTree : forall (x y : LTree), {x = y} + {x <> y}.forall x y : LTree, {x = y} + {x <> y}
Proof.forall x y : LTree, {x = y} + {x <> y}
  decide equality; auto.x, y, x0: LTree
H: forall x1 : LTree, {x0 = x1} + {x0 <> x1}
y0: RTree
x1: LTree
y1: RTree
a: x0 = x1
{y0 = y1} + {y0 <> y1}

This leaves me with the goal:

1 subgoal

  x, y, x0 : LTree
  H : forall x1 : LTree, {x0 = x1} + {x0 <> x1}
  y0 : RTree
  x1 : LTree
  y1 : RTree
  a : x0 = x1
  ============================
  {y0 = y1} + {y0 <> y1}

But I can't solve that until I've derived equality for RTree, which will have the same problem.

Answer

You can use decide equality in this case if you prove the two lemmas for LTrees and RTrees simultaneously:

Lemma eq_LTree : forall (x y : LTree), {x = y} + {x <> y}
with  eq_RTree : forall (x y : RTree), {x = y} + {x <> y}.eq_LTree: forall x y : LTree, {x = y} + {x <> y}
eq_RTree: forall x y : RTree, {x = y} + {x <> y}
forall x y : LTree, {x = y} + {x <> y}
eq_LTree: forall x y : LTree, {x = y} + {x <> y}
eq_RTree: forall x y : RTree, {x = y} + {x <> y}
forall x y : RTree, {x = y} + {x <> y}
Proof.eq_LTree: forall x y : LTree, {x = y} + {x <> y}
eq_RTree: forall x y : RTree, {x = y} + {x <> y}
forall x y : LTree, {x = y} + {x <> y}
eq_LTree: forall x y : LTree, {x = y} + {x <> y}
eq_RTree: forall x y : RTree, {x = y} + {x <> y}
forall x y : RTree, {x = y} + {x <> y}
  -eq_LTree: forall x y : LTree, {x = y} + {x <> y}
eq_RTree: forall x y : RTree, {x = y} + {x <> y}
forall x y : LTree, {x = y} + {x <> y} decide equality.
  -eq_LTree: forall x y : LTree, {x = y} + {x <> y}
eq_RTree: forall x y : RTree, {x = y} + {x <> y}
forall x y : RTree, {x = y} + {x <> y} decide equality.
Qed.

Q: This is strange, Guarded complains after the first decide equality, but then Qed is not rejected.

A: Never mind, I found a thread on coq-club discussing this particular problem.