proposition: Fact eq_gen { X } (P : X -> Type) x : (forall y, y = x -> P y) -> P x.
proof: Proof. intros H; apply H, eq_refl. Qed.
imports: Arith Eqdep_dec Undecidability.Shared(DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec.Util(recalg)