# Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?

If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit:

UnitType = (t : *) -> t -> t
Unit = \(t : *) (x : t). x


And the add the following construct indUnit:

G |- P : UnitType -> *
G |- pu : P Unit
G |- u : UnitType
--------------
G |- indUnit P pu u : P u


With reduction rule:

indUnit P pu Unit ~> pu


Basically this adds induction over the Church-encoded unit type.

1. Is this consistent?
2. If we change the reduction rule to:
indUnit P pu x ~> x (P x) pu (if x is a closed term)


Is it still consistent?

It seems to me that this is consistent.