어차피 지원할 수 있는 연산이 치환 밖에 없어서,
그냥 람다 추상화를 지원하는 게 나을 듯.
#func for_all(t → bool) : bool
#rule for_all_intro(bool) : bool
{
___ (Hyps |- A) => (Hyps |- for_all($x → A))
___ ___ $x ~ Hyps
}
#rule for_all_elim(bool) : bool
{
___ (Hyps |- for_all(A)) => (Hyps |- A T)
}
#rule equal_elim(bool, bool) : bool
{
___ (Hyps |- equal(T, S)), (Hyps |- A T) => (Hyps |- A S)
___ (Hyps |- equal(T, S)), (Hyps |- A S) => (Hyps |- A T)
}