Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?
Yes, it's consistent. Probably the easiest account is in my 2013 CSL paper with Derek Dreyer, Internalizing Parametricity in the Extensional Calculus of Construction, which is all about adding this style of parametricity axiom to the CoC.