fact: Definition beqI (t u : term) := match t, u with | Var x, Var y => beq_nat x y | Fun f _, Fun g _ => beq_symb f g | _, _ => false end.
imports: CoLoR(ATrs LogicUtil ListUtil VecUtil BoolUtil EqUtil ASemLab SN NatUtil RelUtil AWFMInterpretation)