[isabelle] Question concerning HOAS

Dear Isabelle-Community!

Given the following definition of a tree:

datatype myTree =
| bin_node "myTree" "myTree"
| inf_node "nat => myTree"

I would like to prove that trees are acyclic. But I do not even have an idea how to prove the following lemma

lemma "t n \<noteq> bin_node T (inf_node t)"

I would greatly appreciate any hints!

Best regards,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.