You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
6 lines
137 B
6 lines
137 B
let
|
|
congComp : {A B : Type} (f : A -> B) {x : A}
|
|
-> cong f (refl {A} {x}) == refl {B} {f x};
|
|
congComp f = refl;
|
|
|
|
congComp
|