# Is there a systematic method for constructing lambda calculus terms that can distinguish between inputs?

For example, finding terms $\vec{a}$ such that:

$\vec{a}(\lambda x.x) = T\\\vec{a}(\lambda xy.x) = F$

Is there a systematic method for finding terms with these types of constraint?

The Böhm-out technique can construct term contexts that can distinguish between terms iff they are distinct in the beta-eta theory (i.e., a term context $C[-]$ so that $C[s]=T$ and $C[t]=F$). See, e.g., http://www.di.unito.it/~dezani/papers/dgp.pdf - it is exceedingly systemtic.
If the terms are closed, as in your example, the context you construct using the Böhm-out technique will be a term M that you apply to the two terms (so $M s = T$, $M t=F$). Otherwise the term context will include capturing substitutions so that it can work at the sites of the free variables.
You might want to look at Barry Jay's Pattern Calculus. This is something beyond the $\lambda$-calculus, but is has the power to do intensional analysis of lambda expressions.