lean issue

foo.lean

namespace foo

	definition bool := ∀ a : Prop, a → a → a
	definition tt : bool := λ (a : Prop) (c d : a), c
	definition ff : bool := λ (a : Prop) (c d : a), d

	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
	check ind_on

end foo