rfl
case refl
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
irr✝ : ∀ {x : VR}, ¬dj₁ x x
symm✝ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₁, irr := irr✝, symm := symm✝ } a b
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₁, irr := irr✝, symm := symm✝ }
no goals