Drop some the coqtop output, rephrase a bit

1 files changed, 22 insertions, 17 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index c36911e576..b125d21a3c 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1110,7 +1110,7 @@ between universes for inductive types in the Type hierarchy.
 
 .. example:: Non strictly positive occurrence
 
-   It is less obvious why inductive definitions with occurences
+   It is less obvious why inductive type definitions with occurences
    that are positive but not strictly positive are harmful.
    We will see that in presence of an impredicative type they
    are unsound:
@@ -1119,9 +1119,12 @@ between universes for inductive types in the Type hierarchy.
 
       Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
-   If we were to accept this definition we could derive a
-   contradiction by creating an injective function from
-   :math:`A → \Prop` to :math:`A`.
+   If we were to accept this definition we could derive a contradiction
+   by creating an injective function from :math:`A → \Prop` to :math:`A`.
+
+   This function is defined by composing the injective constructor of
+   the type :math:`A` with the function :math:`λx. λz. z = x` injecting
+   any type :math:`T` into :math:`T → \Prop`.
 
    .. coqtop:: none
 
@@ -1129,20 +1132,19 @@ between universes for inductive types in the Type hierarchy.
       Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
       Set Positivity Checking.
 
-   To make this injection we compose the (injective) constructor of
-   the type :math:`A` with the injective function :math:`λz. z = x`.
-
    .. coqtop:: all
 
       Definition f (x: A -> Prop): A := introA (fun z => z = x).
 
+   .. coqtop:: in
+
       Lemma f_inj: forall x y, f x = f y -> x = y.
       Proof.
-        unfold f. intros ? ? H. injection H.
-        set (F := fun z => z = y). intro HF.
-        symmetry. replace (y = x) with (F y).
-        + unfold F. reflexivity.
-        + rewrite <- HF. reflexivity.
+        unfold f; intros ? ? H; injection H.
+        set (F := fun z => z = y); intro HF.
+        symmetry; replace (y = x) with (F y).
+        + unfold F; reflexivity.
+        + rewrite <- HF; reflexivity.
       Qed.
 
    The type :math:`A → \Prop` can be understood as the powerset
@@ -1155,18 +1157,21 @@ between universes for inductive types in the Type hierarchy.
       Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x.
       Definition fd: A := f d.
 
+   .. coqtop:: in
+
       Lemma cantor: (d fd) <-> ~(d fd).
       Proof.
         split.
-        + intros [s [H1 H2]]. unfold fd in H1.
-          replace d with s. assumption.
-          apply f_inj. congruence.
-        + intro. exists d. split. reflexivity. assumption.
+        + intros [s [H1 H2]]; unfold fd in H1.
+          replace d with s.
+          * assumption.
+          * apply f_inj; congruence.
+        + intro; exists d; tauto.
       Qed.
 
       Lemma bad: False.
       Proof.
-        pose cantor. tauto.
+        pose cantor; tauto.
       Qed.
 
    This derivation was first presented by Thierry Coquand and Christine