Theorem twooutofsixv {X Y Z K : UU} {u : X -> Y} {v : Y -> Z} {w : Z -> K} (isuv : isweq (funcomp u v))(isvw : isweq (funcomp v w)) : isweq v. Proof. intros. exact (twooutof3b _ _ (twooutofsixu isuv isvw) isuv). Defined.