fact: Fixpoint ifv (i : index) : set fvar := match i with | IFVar x => \{x} | IBVar _ | Z => \{} | Plus1 i => ifv i | IAbs _ i => ifv i | IApp i1 i2 => ifv i1 \u ifv i2 end.
imports: Equations(Equations) Arith List ListSet Lia Program