Definition Size := R (.\ "Size", "t"; "t" (.\"n"; !(enc 1))
                                          (.\"t1", "t2"; !Add ("Size" "t1") ("Size" "t2"))
                                          (.\"t"; !Add !(enc 1) ("Size" "t")) ).

Lemma Size_correct s : Size (tenc s) == enc (size s).

Lemma size_surj n : ∃ t, size t = S n.