Is Bool injective

theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool v y)    (hxy : MJoin Red x y) : u = v := by  have h : MJoin Red (if u then S else K) (if v then S else K) := by    apply mJoin_red_equivalence.trans (y := x ⬝ S ⬝ K)    · apply mJoin_red_equivalence.symm      apply Relation.MJoin.single      exact hx S K    · apply mJoin_red_equivalence.trans (y := y ⬝ S ⬝ K)      · exact mJoin_red_head K <| mJoin_red_head S hxy      · apply Relation.MJoin.single        exact hy S K  grind [sk_nequiv, mJoin_red_equivalence.symm h]