Step
*
of Lemma
testsq
λx.(x + 2) ~ λx.(x + 1 + 1)
BY
{ RepeatFor 2 (EqCD) }
1
1. x : Base
⊢ x ~ x
2
1. x : Base
⊢ 2 ~ 1 + 1
Latex:
Latex:
\mlambda{}x.(x + 2) \msim{} \mlambda{}x.(x + 1 + 1)
By
Latex:
RepeatFor 2 (EqCD)
Home
Index