Lambda[a](b) : b(a).
Application(b(a), a) : b.
Application(Lambda[$x](s), t) := s[$x:=t].
And[a][b] ::= Pair(a, b).
Fst(And[a][b]) : a.
Fst(Pair(t, s)) := t.
Snd(And[a][b]) : b.
Snd(Pair(t, s)) := s.
Or[a][b] ::= Inl(a), Inr(b).
Case(Or[a][b], c(a), c(b)) : c.
Case(Inl(t), f, _) := f(t).
Case(Inr(t), _, f) := f(t).

TypeConstant[type_var]...[type_var] ::= Constructor_1[type]...[type](type, ..., type),
...,
Constructor_n[type]...[type](type, ..., type).
TermConstant[type]...[type](type, ..., type) : type.
TermConstant[atom]...[atom](term, ..., term) := term.