Rice

theorem rice {P : SKI} (hP : ∀ x : SKI, ((P ⬝ x) ↠ TT) ∨ (P ⬝ x) ↠ FF)    (hxt : ∃ x : SKI, (P ⬝ x) ↠ TT) (hxf : ∃ x : SKI, (P ⬝ x) ↠ FF) : False := by  obtain ⟨a, ha⟩ := hxt  obtain ⟨b, hb⟩ := hxf  let Neg : SKI := P ⬝' &0 ⬝' b ⬝' a |>.toSKI (n := 1)  let Abs : SKI := Neg.fixedPoint  have Neg_app : ∀ x : SKI, (Neg ⬝ x) ↠ P ⬝ x ⬝ b ⬝ a :=    fun x => (P ⬝' &0 ⬝' b ⬝' a) |>.toSKI_correct (n := 1) [x] (by simp)  cases hP Abs  case inl h =>    have : (P ⬝ Abs) ↠ FF := calc      _ ↠ P ⬝ (Neg ⬝ Abs) := by apply MRed.tail; apply fixedPoint_correct      _ ↠ P ⬝ (P ⬝ Abs ⬝ b ⬝ a) := by apply MRed.tail; apply Neg_app      _ ↠ P ⬝ (TT ⬝ b ⬝ a) := by apply MRed.tail; apply MRed.head; apply MRed.head; exact h      _ ↠ P ⬝ b := by apply MRed.tail; apply TT_correct      _ ↠ FF := hb    exact TF_nequiv <| MRed.diamond h this  case inr h =>    have : (P ⬝ Abs) ↠ TT := calc      _ ↠ P ⬝ (Neg ⬝ Abs) := by apply MRed.tail; apply fixedPoint_correct      _ ↠ P ⬝ (P ⬝ Abs ⬝ b ⬝ a) := by apply MRed.tail; apply Neg_app      _ ↠ P ⬝ (FF ⬝ b ⬝ a) := by apply MRed.tail; apply MRed.head; apply MRed.head; exact h      _ ↠ P ⬝ a := by apply MRed.tail; apply FF_correct      _ ↠ TT := ha    exact TF_nequiv <| MRed.diamond this h