Skip to content
Snippets Groups Projects
Commit d4bf79dc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Style tweak.

parent cf73e508
No related branches found
No related tags found
No related merge requests found
...@@ -407,7 +407,7 @@ Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) ...@@ -407,7 +407,7 @@ Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
(S : relation C) (f : A B C) : Prop := (S : relation C) (f : A B C) : Prop :=
inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) R1 x1 y1 R2 x2 y2. inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) R1 x1 y1 R2 x2 y2.
Class Cancel {A B} (S : relation B) (f : A B) (g : B A) : Prop := Class Cancel {A B} (S : relation B) (f : A B) (g : B A) : Prop :=
cancel : x, S (f (g x)) x. cancel x : S (f (g x)) x.
Class Surj {A B} (R : relation B) (f : A B) := Class Surj {A B} (R : relation B) (f : A B) :=
surj y : x, R (f x) y. surj y : x, R (f x) y.
Class IdemP {A} (R : relation A) (f : A A A) : Prop := Class IdemP {A} (R : relation A) (f : A A A) : Prop :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment