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