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