CLEANUP PROPOSITION: existing example was removed because it is not urgently needed

1 files changed, 0 insertions, 10 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index d512df3b78..e5307ef1ec 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1663,16 +1663,6 @@ Below is a typing rule for the term shown in the previous example:
   }
 {\WTEG{\Case{P}{t}{f_1|f_2}}{(P~t)}}}
 
-\[\frac{
-     \begin{array}[b]{@{}c@{}} 
-H:(\haslengthA~L~N) \\ P:\forall l:\ListA, \forall n:\nat, (\haslengthA~l~n)\ra
-  \Prop\\
- f_1:(P~(\Nil~A)~\nO~\nilhl) \\
-   f_2:\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
-  h:(\haslengthA~l~n), (P~(\cons~A~a~n)~(\nS~n)~(\conshl~A~a~l~n~h)) 
-      \end{array}}
-    {\Case{P}{H}{f_1~|~f_2}:(P~L~N~H)}\]
-
 \paragraph[Definition of $\iota$-reduction.]{Definition of $\iota$-reduction.\label{iotared}
 \index{iota-reduction@$\iota$-reduction}}
 We still have to define the $\iota$-reduction in the general case.