htmldoc regenerated

1 files changed, 55 insertions, 0 deletions

diff --git a/docs/htmldoc/mathcomp.ssreflect.ssrbool.html b/docs/htmldoc/mathcomp.ssreflect.ssrbool.html
index dcb9a81..baaddd6 100644
--- a/docs/htmldoc/mathcomp.ssreflect.ssrbool.html
+++ b/docs/htmldoc/mathcomp.ssreflect.ssrbool.html
@@ -19,6 +19,61 @@
 <h1 class="libtitle">Library mathcomp.ssreflect.ssrbool</h1>
 
 <div class="code">
+
+<br/>
+</div>
+
+<div class="doc">
+ Local additions:                                                           
+      {pred T} == a type convertible to pred T but that presents the        
+                  pred_sort coercion class.                                 
+  PredType toP == the predType structure for toP : A -&gt; pred T.             
+    relpre f r == the preimage of r by f, simplifying to r (f x) (f y).     
+&gt; These will become part of the core SSReflect library with Coq 8.11.    
+ This file also anticipates a v8.11 change in the definition of simpl_pred  
+ to T -&gt; simpl_pred T. This change ensures that inE expands the definition  
+ of r : simpl_rel along with the \in, when rewriting in y \in r x.           
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="64f8873130736b599801d4930af00e74"><span class="id" title="notation">&quot;</span></a>{ 'pred' T }" := (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_sort"><span class="id" title="projection">pred_sort</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <span class="id" title="var">T</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
+&nbsp;&nbsp;<span class="id" title="var">format</span> "{ 'pred'  T }") : <span class="id" title="var">type_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="simpl_pred_sortE"><span class="id" title="lemma">simpl_pred_sortE</span></a> <span class="id" title="var">T</span> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#SimplPred"><span class="id" title="definition">SimplPred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ <span class="id" title="keyword">Definition</span> <a name="inE"><span class="id" title="definition">inE</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#inE"><span class="id" title="definition">inE</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#simpl_pred_sortE"><span class="id" title="lemma">simpl_pred_sortE</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="PredType"><span class="id" title="definition">PredType</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">T</span> <span class="id" title="var">pT</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#pT"><span class="id" title="variable">pT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Defined</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="simpl_rel"><span class="id" title="definition">simpl_rel</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#simpl_pred"><span class="id" title="definition">simpl_pred</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="SimplRel"><span class="id" title="definition">SimplRel</span></a> {<span class="id" title="var">T</span>} (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#simpl_rel"><span class="id" title="definition">simpl_rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#SimplPred"><span class="id" title="definition">SimplPred</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#x"><span class="id" title="variable">x</span></a>).<br/>
+<span class="id" title="keyword">Coercion</span> <span class="id" title="var">rel_of_simpl_rel</span> <span class="id" title="var">T</span> (<span class="id" title="var">sr</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#simpl_rel"><span class="id" title="definition">simpl_rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#sr"><span class="id" title="variable">sr</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">&quot;</span></a>[ 'rel' x y | E ]" := (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#SimplRel"><span class="id" title="definition">SimplRel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <span class="id" title="var">E</span>%<span class="id" title="var">B</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
+&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>, <span class="id" title="var">format</span> "'[hv' [ 'rel'  x  y  | '/ '  E ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">&quot;</span></a>[ 'rel' x y : T | E ]" := (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#SimplRel"><span class="id" title="definition">SimplRel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="var">T</span> ⇒ <span class="id" title="var">E</span>%<span class="id" title="var">B</span>)) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
+&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">fun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">&quot;</span></a>[ 'rel' x y 'in' A &amp; B | E ]" :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">B</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&amp;&amp;</span></a> <span class="id" title="var">E</span><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">]</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>,<br/>
+&nbsp;&nbsp;<span class="id" title="var">format</span> "'[hv' [ 'rel'  x  y  'in'  A  &amp;  B  | '/ '  E ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">&quot;</span></a>[ 'rel' x y 'in' A &amp; B ]" := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <span class="id" title="var">B</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>,<br/>
+&nbsp;&nbsp;<span class="id" title="var">format</span> "'[hv' [ 'rel'  x  y  'in'  A  &amp;  B ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="66e9b5543ed85187fbf7ebcaedd62614"><span class="id" title="notation">&quot;</span></a>[ 'rel' x y 'in' A | E ]" := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">&amp;</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">|</span></a> <span class="id" title="var">E</span><a class="idref" href="mathcomp.ssreflect.ssrbool.html#2444a0b5464febf9779b4a3a2d16d148"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>,<br/>
+&nbsp;&nbsp;<span class="id" title="var">format</span> "'[hv' [ 'rel'  x  y  'in'  A  | '/ '  E ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="ec5017d807eee89c28338ba21727b646"><span class="id" title="notation">&quot;</span></a>[ 'rel' x y 'in' A ]" := <a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">in</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">&amp;</span></a> <span class="id" title="var">A</span><a class="idref" href="mathcomp.ssreflect.ssrbool.html#52c6a7c609224dbf167ece67c0159e06"><span class="id" title="notation">]</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
+&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">y</span> <span class="id" title="var">ident</span>, <span class="id" title="var">format</span> "'[hv' [ 'rel'  x  y  'in'  A ] ']'") : <span class="id" title="var">fun_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="xrelpre"><span class="id" title="abbreviation">xrelpre</span></a> := (<span class="id" title="keyword">fun</span> <span class="id" title="var">f</span> (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <a class="idref" href="mathcomp.ssreflect.ssrbool.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#y"><span class="id" title="variable">y</span></a>)).<br/>
+<span class="id" title="keyword">Definition</span> <a name="relpre"><span class="id" title="definition">relpre</span></a> {<span class="id" title="var">T</span> <span class="id" title="var">rT</span>} (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#rT"><span class="id" title="variable">rT</span></a>)  (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#rT"><span class="id" title="variable">rT</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.ssrbool.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#y"><span class="id" title="variable">y</span></a>)<a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">]</span></a>.<br/>
 </div>
 </div>