λx.(x + 2) ~ λx.(x + 1 + 1)
{ RepeatFor 2 (EqCD) }
1. x : Base
⊢ x ~ x
⊢ 2 ~ 1 + 1