| Description: A context has type
boolean.
This and the next few axioms are not strictly necessary, and are
conservative on any theorem for which every variable has a specified
type, but by adding this axiom we can save some typehood hypotheses in
many theorems. The easy way to see that this axiom is conservative is
to note that every axiom and inference rule that constructs a theorem of
the form    where and are type variables, also
ensures that   and .
Thus it is impossible to
prove any theorem  unless both and
had been previously derived, so it is conservative to
deduce from
. The same remark applies to
the construction of the theorem     - there is only one
rule that creates a formula of this type, namely wct 48, and
it requires
that and be previously
established, so it is
safe to reverse the process in wctl 33 and wctr 34.
(Contributed by
Mario Carneiro, 8-Oct-2014.) |
