diff --git a/trees/sga1/sga1-i/sga1-i.7.tree b/trees/sga1/sga1-i/sga1-i.7.tree
index 6823967..43c9917 100644
--- a/trees/sga1/sga1-i/sga1-i.7.tree
+++ b/trees/sga1/sga1-i/sga1-i.7.tree
@@ -13,8 +13,8 @@
   \p{
     Let #{A} be a Noetherian ring, #{B} an algebra which is finite over #{A}, and #{u} a generator of #{B} over #{A}.
     Let #{F\in A[t]} be such that #{F(u)=0} (we do not assume #{F} to be monic), and #{u'=F'(u)} (where #{F'} is the differentiated polynomial).
-    Let #{\frak{q}} be a prime ideal of #{B} not containing #{u'}, and #{\frak{p}} its intersection with #{A}.
-    Then #{B_\frak{q}} is unramified over #{A_\frak{p}}.
+    Let #{\mathfrak{q}} be a prime ideal of #{B} not containing #{u'}, and #{\mathfrak{p}} its intersection with #{A}.
+    Then #{B_\mathfrak{q}} is unramified over #{A_\mathfrak{p}}.
   }
 }
 
@@ -46,7 +46,7 @@
   \number{I.7.3}
 
   \p{
-    Under the conditions of \ref{sga1-i.7.1}, and supposing that #{F} is monic and that #{A[t]/FA[t]\to B} is an isomorphism, in order for #{B_\frak{q}} to be étale over #{A_\frak{p}} it is necessary and sufficient that #{\frak{q}} not contain #{u'}.
+    Under the conditions of \ref{sga1-i.7.1}, and supposing that #{F} is monic and that #{A[t]/FA[t]\to B} is an isomorphism, in order for #{B_\mathfrak{q}} to be étale over #{A_\mathfrak{p}} it is necessary and sufficient that #{\mathfrak{q}} not contain #{u'}.
   }
 
   \proof{
@@ -88,7 +88,157 @@
 
   \proof{
     \p{
-      We
+      We only have to prove necessity.
+      Suppose that #{B} is unramified over #{A}, and thus that #{L} is separable over #{k}.
+      It then follows from the hypotheses that #{L/k} admits a generator #{\xi}, and so the #{\xi^i} (for #{0\leq i<n}) form a basis for #{L} over #{k}.
+      Let #{u\in B} be a lift of #{\xi};
+      by Nakayama, the #{u^i} (for #{0\leq i<n}) generate (resp. form a basis of) the #{A}-module #{B}, and, in particular, we obtain a monic polynomial #{F\in A[t]} such that #{F(u)=0};
+      then #{B} is isomorphic to a quotient of (resp. isomorphic to) #{A[t]/FA[t]}.
+      Finally, by applying \ref{sga1-i.7.4} to #{L/k}, we see that #{F} and #{F'} generate #{A[t]} modulo #{\mathfrak{m}A[t]}, and so (by Nakayama in #{A[t]/FA[t]}) #{F} and #{F'} generate #{A[t]}, and we are done.
     }
   }
 }
+
+\subtree[sga1-i.7.6]{
+  \taxon{theorem}
+  \number{I.7.6}
+
+  \p{
+    Let #{A} be a local ring, and #{A\to\sh{O}} a local homomorphism such that #{\sh{O}} is isomorphic to the localisation of an algebra of finite type over #{A}.
+    Suppose that #{\sh{O}} is \em{unramified} over #{A}.
+    Then we can find an #{A}-algebra #{B} that is integral over #{A}, a maximal ideal #{\mathfrak{n}} of #{B}, a generator #{u} of #{B} over #{A}, and a monic polynomial #{F\in A[t]} such that #{\mathfrak{n}\not\ni F'(u)} and such that #{\sh{O}} is isomorphic (as an #{A}-algebra) to #{B_\mathfrak{n}}.
+    If #{\sh{O}} is étale over #{A}, then we can take #{B=A[t]/FA[t]}.
+  }
+}
+
+\p{
+  (Of course, these conditions are more than sufficient ...)
+}
+
+\p{
+  Before proving \ref{sga1-i.7.6}, we first state some nice corollaries:
+}
+
+\subtree[sga1-i.7.7]{
+  \taxon{corollary}
+  \number{I.7.7}
+
+  \p{
+    For #{\sh{O}} to be unramified over #{A}, it is necessary and sufficient that #{\sh{O}} be isomorphic to the quotient of an algebra which is unramified and \em{étale} over #{A}.
+  }
+
+  \proof{
+    \p{
+      We can take #{\sh{O}'=B'_{\mathfrak{n}'}}, where #{B'=A[t]/FA[t]} and where #{\mathfrak{n}'} is the inverse image of #{\mathfrak{n}} in #{B'}.
+    }
+  }
+}
+
+\subtree[sga1-i.7.8]{
+  \taxon{corollary}
+  \number{I.7.8}
+
+  \p{
+    Let #{f\colon X\to Y} be a morphism of finite type, and #{x\in X}.
+    For #{f} to be unramified at #{x}, it is necessary and sufficient that there exist an open neighbourhood #{U} of #{x} such that #{f|U} factors as #{U\to X'\to Y}, where the first arrow is a closed immersion, and the second is an étale morphism.
+  }
+
+  \proof{
+    \p{
+      This is a simple translation of \ref{sga1-i.7.7}.
+    }
+  }
+}
+
+\p{
+  We will now show how the jargon of \ref{sga1-i.7.6} follows from the main theorem:
+  there exists, by \ref{sga1-i.7.7}, an epimorphism #{\sh{O}'\to\sh{O}}, where #{\sh{O}} has all the desired properties;
+  but since #{\sh{O}'} and #{\sh{O}} are étale over #{A}, the morphism #{\sh{O}'\to\sh{O}} is étale by \ref{sga1-i.4.8}, and thus an isomorphism.
+}
+
+\subtree[sga1-i.7.6-proof]{
+  \taxon{proof of}
+  \number{I.7.6}
+
+  \p{
+    This mimics a proof from the \em{Séminaire Chevalley}.
+    By the "Main Theorem", we have that #{\sh{O}=B_\mathfrak{n}}, where #{B} is an algebra that is finite over #{A}, and #{\mathfrak{n}} is a maximal ideal.
+    Then #{B/\mathfrak{n}=B(\sh{O})} is a separable, and thus monogenous, extension of #{k};
+    if #{\mathfrak{n}_i} (for #{1\leq i\leq r}) are maximal ideas of #{B} that are distinct from #{\mathfrak{n}}, then there thus exists an element #{u} of #{B} that belongs to all the #{\mathfrak{n}_i}, and thus whose image in #{B/\mathfrak{n}} is a generator.
+    But #{B/\mathfrak{n}=B_\mathfrak{n}/\mathfrak{n}B_\mathfrak{n}=B_\mathfrak{n}/\mathfrak{m}B_\mathfrak{n}} (where #{\mathfrak{m}} is the maximal ideal of #{A}).
+
+    Suppose, for the moment, that we have both \ref{sga1-i.7.9} and \ref{sga1-i.7.10}.
+    Let #{n} be the rank of the #{k}-algebra #{L=B\otimes_A k}.
+    By Nakayama, there exists a monic polynomial of degree #{n} in #{A[t]} such that #{F(u)=0}.
+    Let #{f} be the polynomial induced from #{F} by reduction #{\mod\mathfrak{m}}.
+    Then #{L} is #{k}-isomorphic to #{k[t]/fk[t]}, and so, by \ref{sga1-i.7.3}, #{f'(\xi)} is not contained in the maximal ideal of #{L} that corresponds to #{\mathfrak{n}} (where #{\xi} denotes the image of #{t} in #{L}, i.e. the image of #{u} in #{L}).
+    Since #{f'(\xi)} is the image of #{F'(u)}, we are done.
+  }
+}
+
+\subtree[sga1-i.7.9]{
+  \taxon{lemma}
+  \number{I.7.9}
+
+  \p{
+    Let #{A} be a local ring, #{B} an algebra that is finite over #{A}, #{\mathfrak{n}} a maximal ideal of #{B}, and #{u} an element of #{B} whose image in #{B_\mathfrak{n}/\mathfrak{m}B_\mathfrak{n}} is a generator as an algebra over #{k=A/\mathfrak{m}}, and such that #{u} is contained in every maximal ideal of #{B} that is distinct from #{\mathfrak{n}}.
+    Let #{B'=B[u]} and #{\mathfrak{n}'=\mathfrak{n}B'}.
+    Then the canonical homomorphism #{B'_{\mathfrak{n}'}\to B_\mathfrak{n}} is an isomorphism.
+  }
+}
+
+\subtree[sga1-i.7.10]{
+  \taxon{lemma}
+  \number{I.7.10}
+
+  \p{
+    Let #{B} be a algebra that is finite over #{A} and generated by a single element #{u}, and let #{\mathfrak{n}} be a maximal ideal of #{B} such that #{B_\mathfrak{n}} is unramified over #{A}.
+    Then there exists a monic polynomial #{F\in A[t]} such that #{F(u)=0} and #{F'(u)\not\in\mathfrak{n}}.
+  }
+}
+
+\p{
+  N.B. \ref{sga1-i.7.10} should have appeared as a corollary to \ref{sga1-i.7.1}, and before \ref{sga1-i.7.5} (which it implies).
+}
+
+\p{
+  So \ref{sga1-i.7.6} now follows from the combination of \ref{sga1-i.7.9} and \ref{sga1-i.7.10};
+  it remains only to prove \ref{sga1-i.7.9}.
+}
+
+\subtree[sga1-i.7.9-proof]{
+  \taxon{proof of}
+  \number{I.7.9}
+
+  \p{
+    Let #{S'=B'\setminus\mathfrak{n}'}, so that #{B'S'^{-1}=B'_\mathfrak{n'}}.
+    Similarly, let #{S=B\setminus\mathfrak{n}}, so that #{BS^{-1}=B_\mathfrak{n}}.
+    We then have a natural homomorphism #{BS'^{-1}\to BS^{-1}=B_\mathfrak{n}};
+    we will show that this is an isomorphism, i.e. that the elements of #{S} are invertible in #{BS'^{-1}}, i.e. that every maximal ideal #{\mathfrak{p}} of #{BS'^{-1}} does not meet #{S}, i.e. that every maximal ideal of #{BS'^{-1}} induces #{\mathfrak{n}} on #{B}.
+    ##{
+      \begin{CD}
+        B @>>> BS'^{-1} @>>> BS^{-1} = B_\mathfrak{n}
+      \\@AAA @AAA
+      \\B' @>>> B'S'^{-1} = B'_{\mathfrak{n}'}
+      \end{CD}
+    }
+    Since #{BS'^{-1}} is finite over #{B'S'^{-1}=B'_{\mathfrak{n}'}}, #{\mathfrak{p}} induces the unique maximal ideal #{\mathfrak{n}'B_{\mathfrak{n}'}} of #{B'_{\mathfrak{n}'}}, and thus induces the maximal ideal #{\mathfrak{n}'} of #{B'};
+    since #{B} is finite over #{B'}, the ideal #{\mathfrak{q}} of #{B} induced by #{\mathfrak{p}}, which lives over #{\mathfrak{n}'}, is necessarily maximal, and does not contain #{u}, and is thus identical to #{\mathfrak{n}}.
+    (We have just used the fact that #{u} belongs to every maximal ideal of #{B} that is distinct from #{\mathfrak{n}}).
+    We now prove that #{BS'^{-1}} is equal to #{B'S'^{-1}}:
+    since the former is finite over the latter, we can reduce, by Nakayama, to proving equality modulo #{\mathfrak{n}'BS'^{-1}}, and, a fortiori, it suffices to prove equality modulo #{\mathfrak{m}BS'^{-1}};
+    but #{BS'^{-1}/\mathfrak{m}BS'^{-1}=B_\mathfrak{n}/\mathfrak{m}B_\mathfrak{n}} is generated, over #{k}, by #{u} (here we use the other property of #{u}), and so the image of #{B'} (and, a fortiori, of #{B'S'^{-1}}) inside is everything (as a sub-ring that contains #{k} and the image of #{u}.)
+  }
+}
+
+\subtree{
+  \taxon{Remark}
+
+  \p{
+    We must be able to state \ref{sga1-i.7.6} for a ring $\sh{O}$ that is only semi-local, so that we also cover \ref{sga1-i.7.5}:
+    we make the hypothesis that $\sh{O}/\mathfrak{m}\sh{O}$ is a \em{monogenous} $k$-algebra;
+    we can thus find some $u\in B$ whose image in $B/\mathfrak{m}B$ is a generator, and belongs to every maximal ideal of $B$ that doesn't come from $\sh{O}$.
+    Both \ref{sga1-i.7.9} and \ref{sga1-i.7.10} should be able to be adapted without difficulty.
+    More generally, ...
+  }
+}