∀ {n : ℕ} (motive : (x : (_ : Fin n) × Fin n) → x ∈ Equiv.Perm.finPairsLT n → Prop) (x : (_ : Fin n) × Fin n)
  (ha : x ∈ Equiv.Perm.finPairsLT n),
  (∀ (a₁ a₂ : Fin n) (ha : ⟨a₁, a₂⟩ ∈ Equiv.Perm.finPairsLT n), motive ⟨a₁, a₂⟩ ha) → motive x ha