. right; assumption
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ x = y ∨ r i x y
no goals