fact: Fixpoint sty_size (t : sty) := match t with | atom a => 1 | arr s phi t => 1 + sty_size s + list_sum (map sty_size phi) + sty_size t end.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect