Define (coinductively) the notion of bisimilarity on
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.
You may use all the developments made for the preceding exercises in this thread.
Follow this link