proposition: Lemma Acc_arity f i (hi : Acc f i) : i < arity (typ f).
proof: Proof. inversion hi; clear hi; subst; simpl; lia. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite) CoLoR(SN LCall) CoLoR(EqUtil) CoLoR(LCompInt)