Dependent induction principle for Church encoded booleans

bool_ind.lean

namespace foo

definition bool := ∀ a : Type, a → a → a
definition tt : bool := λ (a : Type) (c d : a), c
definition ff : bool := λ (a : Type) (c d : a), d
definition bor (a b : bool) : bool := a bool tt b

definition boolProp := ∀ a : Prop, a → a → a

definition ind_on_T := ∀ P : bool → Prop, ∀ a : bool, P tt → P ff → P a

definition ind_on : ind_on_T := λ (P : bool → Prop) (a : bool) (t : P tt) (f : P ff), a (P a) t f

theorem tt_bor : ∀ (a : boolProp), bor a tt = tt 
    := λ a, ind_on (λ a : boolProp, bor a tt = tt) a rfl rfl

check tt_bor

end foo