apply hyp
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (a b : FormalSum R X), ?r a b → f a = f b

case r
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ FormalSum R X → FormalSum R X → Prop
no goals