let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";;
let eq_refl() = debug (!eqsig Refl) "refl";;
let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";;
let eq_refl() = debug (!eqsig Refl) "refl";;