type mismatch between term's arguments types and the ones defined in the λ scope
term skeleton : (typeA, typeB) -> typeC =
λ (nameA, nameB) : (typeB, typeA) ->
...
this is allowed, and nameA will be of typeB and nameB of type typeA.
Edited by KHAYAM Adam