proposition: Lemma eval_bool_isequiv (f : Bool -> Bool) `{IsEquiv Bool Bool f} : f false = negb (f true).
proof: Proof. pose proof (eissect f true). pose proof (eissect f false). simpl in *. destruct (f true), (f false). - etransitivity; try (eassumption || (symmetry; eassumption)). - simpl. reflexivity. - simpl. reflexivity. - etransitivity; try (eassumption || (symmetry; eassumption)). Defined.
imports: HoTT.Basics Types.Equiv