fact: Fixpoint term_depth(t: term): nat := match t with | tVar x => S (nat_depth x) | tLam A B body => S (max (max (type_depth A) (type_depth B)) (term_depth body)) | tApp t1 t2 => S (max (term_depth t1) (term_depth t2)) | tO => 1 | tS => 1 | tNatRec R => S (type_depth R) end.
imports: Arith Lia List