∀ (α : Type u_1) (β : Type u_2) [inst : LE α] [inst_1 : LE β]
  (motive : ((fun x1 x2 => x1 ≤ x2) ≃r fun x1 x2 => x1 ≤ x2) → Sort u_3) (iso : α ≃ β)
  (h : ∀ {a b : α}, iso a ≤ iso b ↔ a ≤ b)
  (h_1 : (iso : α ≃ β) → (h : ∀ {a b : α}, iso a ≤ iso b ↔ a ≤ b) → motive { toEquiv := iso, map_rel_iff' := h }),
  (match { toEquiv := iso, map_rel_iff' := h } with
    | { toEquiv := iso, map_rel_iff' := h } => h_1 iso h) =
    h_1 iso h