generalize in match (H ? H5);
cases x; intro;
generalize in match (refl_eq ? (a i):a i = a i);
generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;
intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));
generalize in match (H ? H5);
cases x; intro;
generalize in match (refl_eq ? (a i):a i = a i);
generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;
intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));