proposition: Lemma wm_default : forall f, (monP wm) (buildSymInt (defaultIntForSymbol f)).
proof: Proof. Proof with auto. intros. apply sm_imp_wm... Qed.
imports: Coq(Program) CoLoR(ATrs RelUtil SN AWFMInterpretation AMannaNess ACompat ListUtil ARelation LogicUtil OptUtil IntBasedChecker Problem NaryFunction Proof)