fact: Fixpoint eterm_size (u : eterm) : nat := let '(closure ctx t) := u in list_sum (map eterm_size ctx) + (term_size t).
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun