Congruence rules for meta-variables.

[andrejbauer]

Given

rule A type
rule B (a : A) type

we can use congruence B to derive that B x == B y when x == y. But we cannot do the same for a meta-variable, i.e., in

derive (A type) ({a : A} B type) -> ...

how would we show in ... that B{x} == B{y} if x == y? Since meta-variables are just extensions of the signature by new symbols, there should be a congruence rule for them as well. I think we can just make congruence smarter so that it works on a meta-variable. There will be a price to pay: desugaring phase won't be able to check that congruence is applied to the correct number of arguments, because it cannot tell the arity of a meta-variable (I think?).