diomidov

import tactic

abbreviation square_prop {X Y : Type} (R : X → Y → Prop) :=
  ∀ ⦃x₁ x₂ y₁ y₂⦄, R x₁ y₁ → R x₂ y₁ → R x₂ y₂ → R x₁ y₂

inductive the_rel {X Y : Type} (R : X → Y → Prop) : X ⊕ Y → X ⊕ Y → Prop
| fwd {x y} : R x y → the_rel (sum.inl x) (sum.inr y)
| bwd {x y} : R x y → the_rel (sum.inr y) (sum.inl x)
| left {x₁ x₂ y} : R x₁ y → R x₂ y → the_rel (sum.inl x₁) (sum.inl x₂)
| right {x y₁ y₂} : R x y₁ → R x y₂ → the_rel (sum.inr y₁) (sum.inr y₂)