Equality is introduced as an independant parameter, it could be instantiated with Leibniz equality
Require Export Params.
Grammar constr constr1 :=
eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]