fact: Fixpoint ii_open_rec (k : nat) (i : index) (x : fvar) : index := match i with | IBVar n => if eq_nat_dec k n then (IFVar x) else (IBVar n) | IFVar _ | Z => i | Plus1 i => Plus1 (ii_open_rec k i x) | IAbs s i => IAbs s (ii_open_rec (S k) i x) | IApp i1 i2 => IApp (ii_open_rec k i1 x) (ii_open_rec k i2 x) end.
imports: Equations(Equations) Arith List ListSet Lia Program