proposition: Lemma Lemma0_2_4 (A:Type) (B:A->Type) (a1 a2:A) (b1:B a1) (b2:B a2) (p q:a1=a2) (α : p=q) : isweq ((transportf (λ pp, PathOver pp b1 b2) α) : PathOver p b1 b2 -> PathOver q b1 b2).
proof: Proof. induction α. apply idisweq. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA