unif_rule does not convert metavariables into pattern variables

[fblanqui]

constant symbol Set : TYPE;
injective symbol τ : Set → TYPE;

constant symbol prop : Set;
symbol Prop ≔ τ prop;
injective symbol π : Prop → TYPE;

constant symbol ∀ {a} : (τ a → Prop) → Prop;
set quantifier ∀;

set verbose 3;
set flag "print_implicits" on;
set flag "print_domains" on;
set unif_rule π $p ≡ Π x, π $q[x] ↪ [ $p ≡ `∀ x, $q[x] ];
// (hint) [#equiv (π $v0_p) (Π x: $v1, π $v2_q[x]) ↪ #equiv $v0_p (`∀ x: {|?0|}, $v2_q[x])]

// this can later create the following error:
// Uncaught exception: File "src/core/sign.ml", line 191, characters 22-28: Assertion failed.

[fblanqui]

Requires https://github.com/Deducteam/lambdapi/issues/1010 to be fixed first.