proposition: Lemma size_ii_open_rec : forall (i : index) (x : fvar) (rec :nat), index_size (ii_open_rec rec i x) = index_size i.
proof: Proof. intros i x. induction i; intros n; simpl; repeat (match goal with | [ H : forall (_ : nat), _ = _ |- _ ] => rewrite H end); try lia. now destruct (eq_nat_dec _ _). Qed.
imports: Equations(Equations) Arith List ListSet Lia Program