proposition: Lemma absorb_succ_succeq : absorbs_left IR_succ IR_succeq.
proof: Proof. intros x z xz val. apply succ_succeq_compat. destruct xz as [y [ge_xy gt_yz]]. exists (term_int val y). split; auto. Qed.
imports: Coq(Program) CoLoR(ATrs RelUtil SN AWFMInterpretation AMannaNess ACompat ListUtil ARelation LogicUtil OptUtil IntBasedChecker Problem NaryFunction Proof)