fact: Record bijective {A B} (f: A -> B) (invf: B -> A) : Prop := { injective: forall x y, f x = f y -> x = y; surjective: forall x, f (invf x) = x; }.
imports: Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Program.Basics