+nlemma Ax_nAx_equiv :
+ ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
+ C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
+#A; #a; #i; @; #b; #H;
+##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;
+ nwhd in H; ncases H; #x; #E; nrewrite > E;
+ ncases x in E; #b; #Hb; #_; nnormalize; nassumption;
+##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
+ ##[ @ b; nassumption;
+ ##| nnormalize; @; ##]
+##]
+nqed.
+