`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: Tree) (y: RTree).

Lemma eq_LTree : forall (x y : LTree), {x = y} + {x <> y}.
Proof.
    decide equality; auto.

This leaves me with the goal:

y0: RTree
y1: RTree
{y0 = y1} + {y0 <> y1}

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

Answer 1

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}.
Proof.
  decide equality.
  decide equality.
Qed.