proposition: Fact eq_nat_pirr (n m : nat) (H1 H2 : n = m) : H1 = H2.
proof: Proof. apply UIP_dec, eq_nat_dec. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)