fact: Definition arityR (x : Rel): nat := match x with P_ | Q_ => 1 | R_ => 2 | _ => 0 end.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)