proposition: Lemma size_ii_open_rec_lt : forall (i : index) (x : fvar), index_size (ii_open_var i x) < S (index_size i).
proof: Proof. intros; unfold ii_open_var; rewrite size_ii_open_rec. auto with arith. Defined.
imports: Equations(Equations) Arith List ListSet Lia Program