{a b} : (a -> b)%Bool = true <-> (a = true -> b = true). Proof. destruct a; simpl; split; trivial using idpath with nocore; destruct b; simpl; auto using idpath with nocore. Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.