take Free (S,X) ; :: thesis: ( Free (S,X) is X,S -terms & Free (S,X) is strict )
thus ( Free (S,X) is X,S -terms & Free (S,X) is strict ) ; :: thesis: verum