Soundness of Identity Function
This is not the kind of reasoning which the metanotation is intended for, but as a very trivial demonstation of how programs
other than proof tools can do inferences for us we demonstrate that the identity function infers soundly against any specification
in which the input and output languages are the same.
(i.e. given a true proposition it returns the same true proposition)
In the following theorem the ⌜l ↦_{g} l⌝ is the specification, which states that the input and output languages are both ⌜l⌝, and the right hand side of the conditional
asserts that the identity function over ⌜l⌝ satisfies that specification or is sound with respect to that specification.
i.e. when given a true proposition in language ⌜l⌝, it returns a true proposition in the same language.
The specification does not require the output proposition to be the same as the input proposition, but in this case it is.


