inductive Lam : Type where
| S : Lam
| K : Lam
| app : Lam → Lam → Lam
instance : CoeFun Lam (fun _ => Lam → Lam) where
coe lambda := Lam.app lambda
namespace Lam
axiom K_def {a b : Lam} : K a b = a
axiom S_def {a b c : Lam} : S a b c = (a c) (b c)
theorem eta_simp {a b : Lam} : (∀(c : Lam), a c = b c) → a = b := by
intro h
specialize h S
injection h
def I := S K K
theorem I_def {a : Lam} : I a = a := by rw [I, S_def, K_def]
example {a : Lam} : S K a = I := by
apply eta_simp
intro c
rw [I_def, S_def, K_def]
end Lam