λR. λx. λy. (R x y) ∨ (x = y)

Definition RC : forall (A:Type), (A -> A -> Prop) -> A -> A -> Prop := fun (A:Type) => fun (R:(A -> A -> Prop)) => fun (x:A) => fun (y:A) => connectives.Or (R x y) (logic.eq (A) x y)

definition RC : \forall A : Type[0] . (A -> A -> Prop) -> A -> A -> Prop := \lambda A : Type[0]. \lambda R : A -> A -> Prop. \lambda x : A. \lambda y : A. (Or) (R x y) ((eq) (A) x y)

def RC : forall (A : Type) , ((A) -> (A) -> Prop) -> (A) -> (A) -> Prop := fun (A : Type) , fun (R : (A) -> (A) -> Prop) , fun (x : A) , fun (y : A) , (((connectives.Or) ) (((R) (x)) (y))) ((((logic.eq_) (A)) (x)) (y))

RC [A:TYPE+] : [[A -> [A -> bool]] -> [A -> [A -> bool]]] = (LAMBDA(R:[A -> [A -> bool]]):(LAMBDA(x:A):(LAMBDA(y:A):connectives_sttfa_th.sttfa_Or(R(x)(y))(logic_sttfa_th.eq[A](x)(y)))))

Printing for OpenTheory is not working at the moment.