proposition: Lemma Acc_ok f i (hi : Acc f i) a : occurs a (Vnth (inputs (typ f)) (Acc_arity hi)) -> a <B output_base (typ f) \/ (a = output_base (typ f) /\ pos a (Vnth (inputs (typ f)) (Acc_arity hi))).
proof: Proof. inversion hi; subst; simpl; clear hi. fo. 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)