proposition: 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: Proof. intros. exact (twooutof3b _ _ (twooutofsixu isuv isvw) isuv). Defined.
imports: UniMath.Foundations.Preamble