fact: Fixpoint index_size (i : index) : nat := match i with | IBVar _ | IFVar _ | Z => 0 | Plus1 i | IAbs _ i => 1 + index_size i | IApp i1 i2 => 1 + (index_size i1 + index_size i2) end.
imports: Equations(Equations) Arith List ListSet Lia Program