그러니까 정확히 제가 한 게 뭐냐면요, 증명보조기를 만드는 데 쓰이는 기술인데,

증명보조기한테 모든 프로퍼티 psi : Term → Formula에 대하여 psi zero → ∀n (psi n → psi (succ n)) → ∀n (psi n)을 공리로 둔다고 말했을 때,

공리에 의하여 plus zero zero = zero → ∀n (plus n zero = zero → plus (succ n) zero = succ n) → ∀n (plus n zero = n)가 성립한다고 말해주면,

증명보조기가 psi가 적절히 인스턴스화되었는지를 확인해서 (여기서는 psi == ＼x → plus x zero = x로 적절하게 인스턴스됐어요) 통과시켜주는 걸

구현했는데, 유한 개의 공리꼴 변수(여기서는 psi 한 개 뿐이에요)을 다루도록 해봤는데, overflow 뜨네요 ㅋㅋㅋㅋㅋ