let
  congComp : {A B : Type} (f : A -> B) {x : A}
          -> cong f (refl {A} {x}) == refl {B} {f x};
  congComp f = refl;
  
congComp