proposition: Lemma K_equiv x y : IsEquiv (KK' x y).
proof: Proof. unshelve eapply (BuildIsEquiv _ _ _ (K'K x y)). - apply KK'sect. - apply K'Ksect. - intros k. induction k; simp KK' KK'sect. * destruct e. reflexivity. * destruct e. unfold KK' at 4; fold (KK' x w k1). fold (KK' _ _ k2). simpl. rewrite IHk1, IHk2. now rewrite ap2_ap, ap_ap2. Qed.
imports: Equations(Equations)