proposition: Lemma toforallpaths_induction (X Y : UU) (f g : X -> Y) (P : (∏ x, f x = g x) -> UU) (H : ∏ e : f = g, P (toforallpaths _ _ _ e)) : ∏ i : (∏ x, f x = g x), P i.
proof: Proof. intros i. rewrite <- (homotweqinvweq (weqtoforallpaths _ f g)). apply H. Defined.
imports: UniMath.Foundations.PartB