Well for theorem proving you need Sigma and Pi types plus some notion of equality. Can you achieve those with Scott or Church encoding?