λf. λg. ∀ x y z, (f x (g y z)) = (g (f x y) (f x z))

Definition distributive : forall (A:Type), (A -> A -> A) -> (A -> A -> A) -> Prop := fun (A:Type) => fun (f:(A -> A -> A)) => fun (g:(A -> A -> A)) => forall (x:A), forall (y:A), forall (z:A), logic.eq (A) (f x (g y z)) (g (f x y) (f x z))

definition distributive : \forall A : Type[0] . (A -> A -> A) -> (A -> A -> A) -> Prop := \lambda A : Type[0]. \lambda f : A -> A -> A. \lambda g : A -> A -> A. \forall (x:A). \forall (y:A). \forall (z:A). (eq) (A) (f x (g y z)) (g (f x y) (f x z))

def distributive : forall (A : Type) , ((A) -> (A) -> A) -> ((A) -> (A) -> A) -> Prop := fun (A : Type) , fun (f : (A) -> (A) -> A) , fun (g : (A) -> (A) -> A) , forall (x:A) , forall (y:A) , forall (z:A) , (((logic.eq_) (A)) (((f) (x)) (((g) (y)) (z)))) (((g) (((f) (x)) (y))) (((f) (x)) (z)))

distributive [A:TYPE+] : [[A -> [A -> A]] -> [[A -> [A -> A]] -> bool]] = (LAMBDA(f:[A -> [A -> A]]):(LAMBDA(g:[A -> [A -> A]]):(FORALL(x:A):(FORALL(y:A):(FORALL(z:A):logic_sttfa_th.eq[A](f(x)(g(y)(z)))(g(f(x)(y))(f(x)(z))))))))

Printing for OpenTheory is not working at the moment.