Support inference for mutually recursive functions

[janmasrovira]

Currently the inference effect is run locally on each function definition. A consequence of this is that the following cannot be inferred:

module M;

inductive Bool {
  false : Bool;
  true : Bool;
};

inductive Nat {
  zero : Nat;
  suc : Nat → Nat;
};

not : _;
not false ≔ true;
not true ≔ false;

odd : _;
even : _;

odd zero ≔ false;
odd (suc n) ≔ even n;

even zero ≔ true;
even (suc n) ≔ odd n;

end;