Since this question (which I just noticed) seems to be in reaction to my first response to your other question, let me explain again that response. The problem was not that I was implicitly assuming you are equating types with propositions. In any case typically it's the other way around: the propositions-as-types analogy says that propositions can be thought of as types, and type theorists often do so. So as Andrej said, if you want to reject this analogy it's hard to do so without mentioning propositions.
However, in
In this case I don't think the confusion had anything to do with propositions vs types. Rather, it was your assumption (in fairness, somewhat obvious on inspection of the question) that well-typed terms are distinct from typing derivations, so that we can speak of multiple derivations for the same well-typed term. Note this distinction makes just as much sense in logic as in type theory (distinguishing "proofs" and "proof verifications"), we just don't typically make it. And just as we don't have to make the distinction in logic, we don't have to make it in type theory.
If you want to make this assumption clear, I think it is best to just say, "I am distinguishing terms from typing derivations". As I alluded to in my second response, this distinction is sometimes called the "Curry view", and the lack of a distinction the "Church view"--but these are somewhat overloaded terms without universally accepted meanings (for example, sometimes people say "Church" and "Curry" for the presence or absence of type annotations in the syntax of terms)lambda abstraction). The Pfenning paper I linked to sorts out some of these issues.
