The dynamically-variadic nature of "congruence" about andromeda HOT 2 CLOSED

Yes, you can use derived rules. These are like rules, but you derive them from existing rules. They take the form derive P1 ... P2 -> C where Pi are premisess (written as in a rule) and C is a computation that computes a judgement (from the premises), the conclusion.

let mycong =
  derive (A type) ({x : A} B type) (a : A) (b : A) (a ≡ b : A as ξ) ->
    congruence B{a} B{b} ξ
;;

rule A type
rule B (x : A) type
rule C (x : A) (y : A) type
rule a : A
rule b : A
rule ξ : a ≡ b : A ;;

mycong A ({x:A} B x) a b ξ ;;

mycong A ({x:A} A) a b ξ ;;

mycong A ({x:A} C x a) a b ξ ;;

from andromeda.

Sorry, I think my example was too simple to get the point across. I had figured out how to write derived rules by reading tests/nucleus/derive.m31. Right now the AML function I'm trying to write cannot itself be replaced by a derived rule, but somewhere inside of it I need to apply a congruence rule where the "head" is an abstracted metavariable supplied by the user, and I was surprised to discover that using congruence was unstable because the form of what the user supplied would change the number of arguments required by congruence. But based on your answer I guess that the solution I had thought of is the intended one, so I'll go that way.

from andromeda.