prove_constructors_injective : thm -> thm
# let ith,rth = define_type "tree = LEAF num | NODE tree tree";; val ith : thm = |- !P. (!a. P (LEAF a)) /\ (!a0 a1. P a0 /\ P a1 ==> P (NODE a0 a1)) ==> (!x. P x) val rth : thm = |- !f0 f1. ?fn. (!a. fn (LEAF a) = f0 a) /\ (!a0 a1. fn (NODE a0 a1) = f1 a0 a1 (fn a0) (fn a1))
# prove_constructors_injective rth;; val it : thm = |- (!a a'. LEAF a = LEAF a' <=> a = a') /\ (!a0 a1 a0' a1'. NODE a0 a1 = NODE a0' a1' <=> a0 = a0' /\ a1 = a1')