fact: Definition enc (x: Symbol) : nat := if sym_eq_dec x a0 then 0 else if sym_eq_dec x b0 then 1 else 2 + ( match x with | (n, None) => enc_pair (n, 0) | (n, Some m) => enc_pair (n, 1 + m) end).
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun