take Free (S,X) ; :: thesis: not Free (S,X) is array-degenerated
thus not Free (S,X) is array-degenerated ; :: thesis: verum