exit
check (λ {T : Prop} (t : T), t) bool.tt
