Given the following primitive recursion theorem for labelled binary trees:
prove_constructors_distinct proves and returns the theorem:
|- !f0 f1.
(!x. fn(LEAF x) = f0 x) /\
(!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
This states that leaf nodes are different from internal nodes. When
the concrete type in question has more than two constructors, the resulting
theorem is just conjunction of inequalities of this kind.
|- !x b1 b2. ~(LEAF x = NODE b1 b2)