# Tree bisimilarity

Define (coinductively) the notion of bisimilarity on
`LTree A`.

Prove that it an equivalence on `LTree A`.

Prove that two trees *t1* and *t2*
are bisimilar if and only if
the function `LTree_label` always returns the same result
for *t1* and *t2*.
### Resources

You may use all the developments made for the preceding exercises in this thread.
## Solution

Follow this link

Going home

Pierre Castéran