proposition: Fact ra_comp_inj k k' i f f' gj gj' : @ra_comp k i f gj = @ra_comp k' i f' gj' -> exists H : k = k', eq_rect _ _ f _ H = f' /\ eq_rect _ _ gj _ H = gj'.
proof: Proof. inj; intros ? ? H; exists H; subst; simpl; diauto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec