(**************************************************************************)
include "basics/relations.ma".
+include "ground_2/xoa/and_3.ma".
+include "ground_2/xoa/ex_2_2.ma".
include "ground_2/lib/logic.ma".
(* GENERIC RELATIONS ********************************************************)
definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝
λA,B,C,D,E,F.A→B→C→D→E→F→Prop.
-(**) (* we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
+(**) (* we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
definition c_reflexive (A) (B): predicate (relation3 A B B) ≝
λR. ∀a,b. R a b b.