fact: Definition arityF (x : Fun): nat := match x with f_ | g_ => 1 | h_ => 2 | _ => 0 end.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)