proposition: Lemma wf_IR_succ : WF IR_succ.
proof: Proof. intros. apply IR_WF. apply succ_wf. Qed.
imports: Coq(Program) CoLoR(ATrs RelUtil SN AWFMInterpretation AMannaNess ACompat ListUtil ARelation LogicUtil OptUtil IntBasedChecker Problem NaryFunction Proof)