let C be initialized ConstructorSignature; :: thesis: for a being expression of C, an_Adj C holds variables_in ((non_op C) term a) = variables_in a
let a be expression of C, an_Adj C; :: thesis: variables_in ((non_op C) term a) = variables_in a
(non_op C) term a = [non_op, the carrier of C] -tree <*a*> by Th43;
hence variables_in ((non_op C) term a) = variables_in a by Th93; :: thesis: verum