We justify reasoning about non-total (partial) functional languages using methods seemingly
only valid for total ones; this permitsfast and loose'reasoning without actually being
loose.\par Two languages are defined, one total and one partial, with identical syntax. The
semantics of the partial language includes partial and infinite values and lifted types,
including lifted function spaces. A partial equivalence relation is then defined, the domain of
which is the total subset of the partial language. It is proved that if two closed terms have the …