proposition: Lemma cong_iter {A B C} (f : A -> B) (g : B -> C) (x y : A) (e : x = y) : Top.cong g (Top.cong f e) = Top.cong (fun x => g (f x)) e.
proof: Proof. revert y e. refine (Top.J _ _). reflexivity. Qed.
imports: Equations Utf8