fact: Definition product_rel {X Y : Type} (A : X -> X -> Prop) (B : Y -> Y -> Prop) := fun x y => A (fst x) (fst y) /\ B (snd x) (snd y).
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)