fact: Fixpoint term_size (t : term) : nat := match t with | var n => S n | app s t => 1 + term_size s + term_size t | lam s => 2 + term_size s end.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun