proposition: Lemma cong_subst2 {A B C} (f : C -> B) (x y : A) (e : x = y) (z w : A -> C) (p : z x = w x) : Top.cong f (Top.subst2 (P:=fun x : A => z x = w x) p y e) = Top.subst2 (P := fun x : A => f (z x) = f (w x)) (Top.cong f p) y e.
proof: Proof. revert y e. refine (Top.J _ _). simpl. reflexivity. Defined.
imports: Equations Utf8