simp only [congr, pcongr]
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
⊢ congr F i x y
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
⊢ ↑(pgfp (precongr F)) ⊥ i x y