Modeling of functions

[bvssvni]

I am gravitating towards using a straightforward way of modeling functions:

true : bool
false : bool
(and(true, true), true)
(and(false, X), false) :- X : bool.
(and(X, false), false) :- X : bool.

This can prove (and(false, false), false).

The type is used as the role, and the tuple is used as a proof that and(false, false) = false, even thought the actual expression would be bool(and(false, false)) = false.