generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.choice.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 771 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.choice.html b/docs/htmldoc/mathcomp.ssreflect.choice.html
new file mode 100644
index 0000000..d38d215
--- /dev/null
+++ b/docs/htmldoc/mathcomp.ssreflect.choice.html
@@ -0,0 +1,771 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>mathcomp.ssreflect.choice</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.ssreflect.choice</h1>
+
+<div class="code">
+<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This file contains the definitions of:                                     
+   choiceType == interface for types with a choice operator.                
+    countType == interface for countable types (implies choiceType).        
+ subCountType == interface for types that are both subType and countType.   
+  xchoose exP == a standard x such that P x, given exP : exists x : T, P x  
+                 when T is a choiceType. The choice depends only on the     
+                 extent of P (in particular, it is independent of exP).     
+   choose P x0 == if P x0, a standard x such that P x.                      
+      pickle x == a nat encoding the value x : T, where T is a countType.   
+    unpickle n == a partial inverse to pickle: unpickle (pickle x) = Some x 
+  pickle_inv n == a sharp partial inverse to pickle pickle_inv n = Some x   
+                  if and only if pickle x = n.                              
+ [choiceType of T for cT] == clone for T of the choiceType cT.              
+        [choiceType of T] == clone for T of the choiceType inferred for T.  
+  [countType of T for cT] == clone for T of the countType cT.               
+        [count Type of T] == clone for T of the countType inferred for T.   
+ [choiceMixin of T by &lt;: ] == Choice mixin for T when T has a subType p      
+                        structure with p : pred cT and cT has a Choice      
+                        structure; the corresponding structure is Canonical.
+  [countMixin of T by &lt;: ] == Count mixin for a subType T of a countType.    
+  PcanChoiceMixin fK == Choice mixin for T, given f : T -&gt; cT where cT has  
+                        a Choice structure, a left inverse partial function 
+                        g and fK : pcancel f g.                             
+   CanChoiceMixin fK == Choice mixin for T, given f : T -&gt; cT, g and        
+                        fK : cancel f g.                                    
+   PcanCountMixin fK == Count mixin for T, given f : T -&gt; cT where cT has   
+                        a Countable structure, a left inverse partial       
+                        function g and fK : pcancel f g.                    
+    CanCountMixin fK == Count mixin for T, given f : T -&gt; cT, g and         
+                        fK : cancel f g.                                    
+      GenTree.tree T == generic n-ary tree type with nat-labeled nodes and  
+                        T-labeled leaves, for example GenTree.Leaf (x : T), 
+                        GenTree.Node 5 [:: t; t' ]. GenTree.tree is equipped 
+                        with canonical eqType, choiceType, and countType    
+                        instances, and so simple datatypes can be similarly 
+                        equipped by encoding into GenTree.tree and using    
+                        the mixins above.                                   
+        CodeSeq.code == bijection from seq nat to nat.                      
+      CodeSeq.decode == bijection inverse to CodeSeq.code.                  
+ In addition to the lemmas relevant to these definitions, this file also    
+ contains definitions of a Canonical choiceType and countType instances for 
+ all basic datatypes (e.g., nat, bool, subTypes, pairs, sums, etc.).         
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Technical definitions about coding and decoding of nat sequences, which    
+ are used below to define various Canonical instances of the choice and     
+ countable interfaces.                                                       
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="CodeSeq"><span class="id" title="module">CodeSeq</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Goedel-style one-to-one encoding of seq nat into nat.                      
+ The code for [:: n1; ...; nk] has binary representation                    
+          1 0 ... 0 1 ... 1 0 ... 0 1 0 ... 0                               
+            &lt;-----&gt;         &lt;-----&gt;   &lt;-----&gt;                               
+             nk 0s           n2 0s     n1 0s                                 
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="CodeSeq.code"><span class="id" title="definition">code</span></a> := <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> ⇒ 2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>) 0.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="CodeSeq.decode_rec"><span class="id" title="definition">decode_rec</span></a> (<span class="id" title="var">v</span> <span class="id" title="var">q</span> <span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">q</span>} :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#q"><span class="id" title="variable">q</span></a>, <a class="idref" href="mathcomp.ssreflect.choice.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| 0, <span class="id" title="var">_</span>         ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;| <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>, 0     ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">rec</span></a> 0<a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;| <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>, 1     ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">rec</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;| <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>, <span class="id" title="var">r'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#793e3499c36e4c6595d810e871a5acdd"><span class="id" title="notation">.+2</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">rec</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <span class="id" title="var">r'</span><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span> <span class="id" title="keyword">where</span> <a name="c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">&quot;</span></a>[ 'rec' v , q , r ]" := (<a class="idref" href="mathcomp.ssreflect.choice.html#decode_rec"><span class="id" title="definition">decode_rec</span></a> <span class="id" title="var">v</span> <span class="id" title="var">q</span> <span class="id" title="var">r</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="CodeSeq.decode"><span class="id" title="definition">decode</span></a> <span class="id" title="var">n</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> 0 <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">rec</span></a> 0<a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.decodeK"><span class="id" title="lemma">decodeK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.decode"><span class="id" title="definition">decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.code"><span class="id" title="definition">code</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.codeK"><span class="id" title="lemma">codeK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.code"><span class="id" title="definition">code</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.decode"><span class="id" title="definition">decode</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.ltn_code"><span class="id" title="lemma">ltn_code</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">j</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.code"><span class="id" title="definition">code</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="CodeSeq.gtn_decode"><span class="id" title="lemma">gtn_decode</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn"><span class="id" title="definition">ltn</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq.decode"><span class="id" title="definition">decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CodeSeq"><span class="id" title="module">CodeSeq</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="OtherEncodings"><span class="id" title="section">OtherEncodings</span></a>.<br/>
+</div>
+
+<div class="doc">
+ Miscellaneous encodings: option T -c-&gt; seq T, T1 * T2 -c-&gt; {i : T1 &amp; T2}   
+ T1 + T2 -c-&gt; option T1 * option T2, unit -c-&gt; bool; bool -c-&gt; nat is       
+ already covered in ssrnat by the nat_of_bool coercion, the odd predicate,  
+ and their "cancellation" lemma oddb. We use these encodings to propagate   
+ canonical structures through these type constructors so that ultimately    
+ all Choice and Countable instanced derive from nat and the seq and sigT    
+ constructors.                                                               
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Variables</span> <a name="OtherEncodings.T"><span class="id" title="variable">T</span></a> <a name="OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a name="OtherEncodings.T2"><span class="id" title="variable">T2</span></a> : <span class="id" title="keyword">Type</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="seq_of_opt"><span class="id" title="definition">seq_of_opt</span></a> := @<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#oapp"><span class="id" title="abbreviation">oapp</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T"><span class="id" title="variable">T</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.seq.html#nseq"><span class="id" title="definition">nseq</span></a> 1) <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="seq_of_optK"><span class="id" title="lemma">seq_of_optK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#seq_of_opt"><span class="id" title="definition">seq_of_opt</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#ohead"><span class="id" title="definition">ohead</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tag_of_pair"><span class="id" title="definition">tag_of_pair</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) := @<a class="idref" href="mathcomp.ssreflect.eqtype.html#Tagged"><span class="id" title="definition">Tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="pair_of_tag"><span class="id" title="definition">pair_of_tag</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">}</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#tag"><span class="id" title="definition">tag</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#tagged"><span class="id" title="definition">tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tag_of_pairK"><span class="id" title="lemma">tag_of_pairK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pair"><span class="id" title="definition">tag_of_pair</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pair_of_tag"><span class="id" title="definition">pair_of_tag</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="pair_of_tagK"><span class="id" title="lemma">pair_of_tagK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pair_of_tag"><span class="id" title="definition">pair_of_tag</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pair"><span class="id" title="definition">tag_of_pair</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="opair_of_sum"><span class="id" title="definition">opair_of_sum</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> | <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">y</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <span class="id" title="keyword">end</span>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="sum_of_opair"><span class="id" title="definition">sum_of_opair</span></a> <span class="id" title="var">p</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#oapp"><span class="id" title="abbreviation">oapp</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#some"><span class="id" title="abbreviation">some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> @<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#omap"><span class="id" title="abbreviation">omap</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings.T2"><span class="id" title="variable">T2</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="opair_of_sumK"><span class="id" title="lemma">opair_of_sumK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#opair_of_sum"><span class="id" title="definition">opair_of_sum</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sum_of_opair"><span class="id" title="definition">sum_of_opair</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bool_of_unitK"><span class="id" title="lemma">bool_of_unitK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#OtherEncodings"><span class="id" title="section">OtherEncodings</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Generic variable-arity tree type, providing an encoding target for         
+ miscellaneous user datatypes. The GenTree.tree type can be combined with   
+ a sigT type to model multi-sorted concrete datatypes.                       
+</div>
+<div class="code">
+<span class="id" title="keyword">Module</span> <a name="GenTree"><span class="id" title="module">GenTree</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="GenTree.Def"><span class="id" title="section">Def</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="GenTree.Def.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Inductive</span> <a name="GenTree.tree"><span class="id" title="inductive">tree</span></a> := <a name="GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Def.T"><span class="id" title="variable">T</span></a> | <a name="GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> &amp; <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">tree</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="GenTree.tree_rect"><span class="id" title="definition">tree_rect</span></a> <span class="id" title="var">K</span> <span class="id" title="var">IH_leaf</span> <span class="id" title="var">IH_node</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fix</span> <span class="id" title="var">loop</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> := <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#IH_leaf"><span class="id" title="variable">IH_leaf</span></a> <span class="id" title="var">x</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> ⇒<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="keyword">fix</span> <span class="id" title="var">iter_pair</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#prod"><span class="id" title="inductive">prod</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> :=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">f'</span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#loop"><span class="id" title="variable">loop</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#iter_pair"><span class="id" title="variable">iter_pair</span></a> <span class="id" title="var">f'</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#IH_node"><span class="id" title="variable">IH_node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> (<a class="idref" href="mathcomp.ssreflect.choice.html#iter_pair"><span class="id" title="variable">iter_pair</span></a> <span class="id" title="var">f0</span>)<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="GenTree.tree_rec"><span class="id" title="definition">tree_rec</span></a> (<span class="id" title="var">K</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.tree"><span class="id" title="inductive">tree</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Set</span>) := @<a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.tree_rect"><span class="id" title="definition">tree_rect</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="GenTree.tree_ind"><span class="id" title="definition">tree_ind</span></a> <span class="id" title="var">K</span> <span class="id" title="var">IH_leaf</span> <span class="id" title="var">IH_node</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fix</span> <span class="id" title="var">loop</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a> := <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#IH_leaf"><span class="id" title="variable">IH_leaf</span></a> <span class="id" title="var">x</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> ⇒<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="keyword">fix</span> <span class="id" title="var">iter_conj</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#and"><span class="id" title="inductive">and</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> :=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">f'</span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#conj"><span class="id" title="constructor">conj</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#loop"><span class="id" title="variable">loop</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#iter_conj"><span class="id" title="variable">iter_conj</span></a> <span class="id" title="var">f'</span>) <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">Logic.I</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#IH_node"><span class="id" title="variable">IH_node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f0</span> (<a class="idref" href="mathcomp.ssreflect.choice.html#iter_conj"><span class="id" title="variable">iter_conj</span></a> <span class="id" title="var">f0</span>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="GenTree.encode"><span class="id" title="definition">encode</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Def.T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">_</span> <span class="id" title="var">x</span><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <span class="id" title="var">f</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> <span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#flatten"><span class="id" title="definition">flatten</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#encode"><span class="id" title="definition">encode</span></a> <span class="id" title="var">f</span>)) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">_</span> 0)<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="GenTree.decode_step"><span class="id" title="definition">decode_step</span></a> <span class="id" title="var">c</span> <span class="id" title="var">fs</span> := <br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inr"><span class="id" title="constructor">inr</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Leaf"><span class="id" title="constructor">Leaf</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> 0 ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#inl"><span class="id" title="constructor">inl</span></a> <span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Node"><span class="id" title="constructor">Node</span></a> <span class="id" title="var">n</span> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#head"><span class="id" title="definition">head</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fs"><span class="id" title="variable">fs</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="GenTree.decode"><span class="id" title="definition">decode</span></a> <span class="id" title="var">c</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#ohead"><span class="id" title="definition">ohead</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.decode_step"><span class="id" title="definition">decode_step</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">).1</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="GenTree.codeK"><span class="id" title="lemma">codeK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.encode"><span class="id" title="definition">encode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.decode"><span class="id" title="definition">decode</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree.Def"><span class="id" title="section">Def</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#GenTree"><span class="id" title="module">GenTree</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tree_eqMixin"><span class="id" title="definition">tree_eqMixin</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) := <a class="idref" href="mathcomp.ssreflect.eqtype.html#PcanEqMixin"><span class="id" title="definition">PcanEqMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#codeK"><span class="id" title="lemma">GenTree.codeK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tree_eqType</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">GenTree.tree</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#tree_eqMixin"><span class="id" title="definition">tree_eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Structures for Types with a choice function, and for Types with countably  
+ many elements. The two concepts are closely linked: we indeed make         
+ Countable a subclass of Choice, as countable choice is valid in CiC. This  
+ apparent redundancy is needed to ensure the consistency of the Canonical   
+ inference, as the canonical Choice for a given type may differ from the    
+ countable choice for its canonical Countable structure, e.g., for options. 
+   The Choice interface exposes two choice functions; for T : choiceType    
+ and P : pred T, we provide:                                                
+    xchoose : (exists x, P x) -&gt; T                                          
+    choose : pred T -&gt; T -&gt; T                                               
+   While P (xchoose exP) will always hold, P (choose P x0) will be true if  
+ and only if P x0 holds. Both xchoose and choose are extensional in P and   
+ do not depend on the witness exP or x0 (provided P x0 holds). Note that    
+ xchoose is slightly more powerful, but less convenient to use.             
+   However, neither choose nor xchoose are composable: it would not be      
+ be possible to extend the Choice structure to arbitrary pairs using only   
+ these functions, for instance. Internally, the interfaces provides a       
+ subtly stronger operation, Choice.InternalTheory.find, which performs a    
+ limited search using an integer parameter only rather than a full value as 
+ [x]choose does. This is not a restriction in a constructive theory, where  
+ all types are concrete and hence countable. In the case of an axiomatic    
+ theory, such as that of the Coq reals library, postulating a suitable      
+ axiom of choice suppresses the need for guidance. Nevertheless this        
+ operation is just what is needed to make the Choice interface compose.     
+   The Countable interface provides three functions; for T : countType we   
+ get pickle : T -&gt; nat, and unpickle, pickle_inv : nat -&gt; option T.         
+ The functions provide an effective embedding of T in nat: unpickle is a    
+ left inverse to pickle, which satisfies pcancel pickle unpickle, i.e.,     
+ unpickle \o pickle =1 some; pickle_inv is a more precise inverse for which 
+ we also have ocancel pickle_inv pickle. Both unpickle and pickle need to   
+ be partial functions to allow for possibly empty types such as {x | P x}.  
+   The names of these functions underline the correspondence with the       
+ notion of "Serializable" types in programming languages.                   
+   Finally, we need to provide a join class to let type inference unify     
+ subType and countType class constraints, e.g., for a countable subType of  
+ an uncountable choiceType (the issue does not arise earlier with eqType or 
+ choiceType because in practice the base type of an Equality/Choice subType 
+ is always an Equality/Choice Type).                                         
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="Choice"><span class="id" title="module">Choice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Choice.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Record</span> <a name="Choice.mixin_of"><span class="id" title="record">mixin_of</span></a> <span class="id" title="var">T</span> := <a name="Choice.Mixin"><span class="id" title="constructor">Mixin</span></a> {<br/>
+&nbsp;&nbsp;<a name="Choice.find"><span class="id" title="projection">find</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>;<br/>
+&nbsp;&nbsp;<span class="id" title="var">_</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> <span class="id" title="var">n</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a>;<br/>
+&nbsp;&nbsp;<span class="id" title="var">_</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>;<br/>
+&nbsp;&nbsp;<span class="id" title="var">_</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>, <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#find"><span class="id" title="method">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a><br/>
+}.<br/>
+
+<br/>
+<span class="id" title="keyword">Record</span> <a name="Choice.class_of"><span class="id" title="record">class_of</span></a> <span class="id" title="var">T</span> := <a name="Choice.Class"><span class="id" title="constructor">Class</span></a> {<a name="Choice.base"><span class="id" title="projection">base</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class_of"><span class="id" title="abbreviation">Equality.class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>; <a name="Choice.mixin"><span class="id" title="projection">mixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>}.<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="Choice.type"><span class="id" title="record">type</span></a> := <a name="Choice.Pack"><span class="id" title="constructor">Pack</span></a> {<a name="Choice.sort"><span class="id" title="projection">sort</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sort"><span class="id" title="method">sort</span></a>; <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span>}.<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Choice.ClassDef.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>) (<a name="Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.type"><span class="id" title="record">type</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="Choice.class"><span class="id" title="definition">class</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">c</span> <span class="id" title="var">_</span> <span class="id" title="keyword">as</span> <span class="id" title="var">cT'</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT'"><span class="id" title="variable">cT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">c</span>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Choice.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">c</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Let</span> <a name="Choice.ClassDef.xT"><span class="id" title="variable">xT</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">T</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Choice.xclass"><span class="id" title="abbreviation">xclass</span></a> := (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">class</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.xT"><span class="id" title="variable">xT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="Choice.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">m</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> <span class="id" title="var">bT</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.class"><span class="id" title="definition">Equality.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bT"><span class="id" title="variable">bT</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Pack</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Class"><span class="id" title="constructor">Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Inheritance  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="Choice.eqType"><span class="id" title="definition">eqType</span></a> := @<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.xclass"><span class="id" title="abbreviation">xclass</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef.xT"><span class="id" title="variable">xT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Import</span> <a name="Choice.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">base</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.base"><span class="id" title="projection">Equality.class_of</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.sort"><span class="id" title="projection">Sortclass</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.eqType"><span class="id" title="definition">Equality.type</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqType</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.type"><span class="id" title="record">type</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Choice.Exports.choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin_of"><span class="id" title="record">mixin_of</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>).<br/>
+<span class="id" title="keyword">Notation</span> <a name="3c4bcf103732e5c03bac4c26d0c2ac12"><span class="id" title="notation">&quot;</span></a>[ 'choiceType' 'of' T 'for' cT ]" :=  (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#idfun"><span class="id" title="abbreviation">idfun</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">format</span> "[ 'choiceType'  'of'  T  'for'  cT ]") : <span class="id" title="var">form_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">&quot;</span></a>[ 'choiceType' 'of' T ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</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">format</span> "[ 'choiceType'  'of'  T ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="Choice.InternalTheory"><span class="id" title="module">InternalTheory</span></a>.<br/>
+<span class="id" title="keyword">Section</span> <a name="Choice.InternalTheory.InternalTheory"><span class="id" title="section">InternalTheory</span></a>.<br/>
+</div>
+
+<div class="doc">
+ Inner choice function.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.find"><span class="id" title="projection">find</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.mixin"><span class="id" title="projection">mixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="Choice.InternalTheory.InternalTheory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.InternalTheory.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Choice.InternalTheory.correct"><span class="id" title="lemma">correct</span></a> <span class="id" title="var">P</span> <span class="id" title="var">n</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Choice.InternalTheory.complete"><span class="id" title="lemma">complete</span></a> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Choice.InternalTheory.extensional"><span class="id" title="lemma">extensional</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Fact</span> <a name="Choice.InternalTheory.xchoose_subproof"><span class="id" title="lemma">xchoose_subproof</span></a> <span class="id" title="var">P</span> <span class="id" title="var">exP</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.find"><span class="id" title="definition">find</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#ex_minn"><span class="id" title="definition">ex_minn</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.complete"><span class="id" title="lemma">complete</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory.InternalTheory"><span class="id" title="section">InternalTheory</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.InternalTheory"><span class="id" title="module">InternalTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice"><span class="id" title="module">Choice</span></a>.<br/>
+<span class="id" title="keyword">Export</span> <span class="id" title="var">Choice.Exports</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="ChoiceTheory"><span class="id" title="section">ChoiceTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>.<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">Choice.InternalTheory</span> <span class="id" title="var">CodeSeq</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.OneType"><span class="id" title="section">OneType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="xchoose"><span class="id" title="definition">xchoose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">exP</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#sval"><span class="id" title="abbreviation">sval</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose_subproof"><span class="id" title="lemma">xchoose_subproof</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="xchooseP"><span class="id" title="lemma">xchooseP</span></a> <span class="id" title="var">P</span> <span class="id" title="var">exP</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_xchoose"><span class="id" title="lemma">eq_xchoose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">exP</span> <span class="id" title="var">exQ</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> @<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exP"><span class="id" title="variable">exP</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> @<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#exQ"><span class="id" title="variable">exQ</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sigW"><span class="id" title="lemma">sigW</span></a> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sig2W"><span class="id" title="lemma">sig2W</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sig_eqW"><span class="id" title="lemma">sig_eqW</span></a> (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<span class="id" title="var">lhs</span> <span class="id" title="var">rhs</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#vT"><span class="id" title="variable">vT</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sig2_eqW"><span class="id" title="lemma">sig2_eqW</span></a> (<span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">lhs</span> <span class="id" title="var">rhs</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#vT"><span class="id" title="variable">vT</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#lhs"><span class="id" title="variable">lhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#rhs"><span class="id" title="variable">rhs</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="choose"><span class="id" title="definition">choose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">x0</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#addfbab002f749a52fe38aa5d236c15e"><span class="id" title="notation">{?</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#addfbab002f749a52fe38aa5d236c15e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#addfbab002f749a52fe38aa5d236c15e"><span class="id" title="notation">}</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#exist"><span class="id" title="constructor">exist</span></a> <span class="id" title="var">x</span> <span class="id" title="var">Px</span>) <span class="id" title="keyword">then</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#xchoose"><span class="id" title="definition">xchoose</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#ex_intro"><span class="id" title="constructor">ex_intro</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3f6d75f5a9cb81b61e8423a7aac22056"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3f6d75f5a9cb81b61e8423a7aac22056"><span class="id" title="notation">eta</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3f6d75f5a9cb81b61e8423a7aac22056"><span class="id" title="notation">]</span></a> <span class="id" title="var">x</span> <span class="id" title="var">Px</span>)<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="chooseP"><span class="id" title="lemma">chooseP</span></a> <span class="id" title="var">P</span> <span class="id" title="var">x0</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="choose_id"><span class="id" title="lemma">choose_id</span></a> <span class="id" title="var">P</span> <span class="id" title="var">x0</span> <span class="id" title="var">y0</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#y0"><span class="id" title="variable">y0</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_choose"><span class="id" title="lemma">eq_choose</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choose"><span class="id" title="definition">choose</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Q"><span class="id" title="variable">Q</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.OneType.CanChoice"><span class="id" title="section">CanChoice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="ChoiceTheory.OneType.CanChoice.sT"><span class="id" title="variable">sT</span></a> : <span class="id" title="keyword">Type</span>) (<a name="ChoiceTheory.OneType.CanChoice.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> <span class="id" title="var">f'</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice.sT"><span class="id" title="variable">sT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <span class="id" title="var">f'</span> (<span class="id" title="var">fK</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#can_pcan"><span class="id" title="lemma">can_pcan</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fK"><span class="id" title="variable">fK</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.CanChoice"><span class="id" title="section">CanChoice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.OneType.SubChoice"><span class="id" title="section">SubChoice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="ChoiceTheory.OneType.SubChoice.P"><span class="id" title="variable">P</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>) (<a name="ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#subType"><span class="id" title="record">subType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.eqtype.html#valK"><span class="id" title="lemma">valK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="sub_choiceClass"><span class="id" title="definition">sub_choiceClass</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Class"><span class="id" title="constructor">Choice.Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#sub_eqMixin"><span class="id" title="definition">sub_eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sub_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Pack"><span class="id" title="constructor">Choice.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceClass"><span class="id" title="definition">sub_choiceClass</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice.sT"><span class="id" title="variable">sT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.SubChoice"><span class="id" title="section">SubChoice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fact</span> <a name="seq_choiceMixin"><span class="id" title="lemma">seq_choiceMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">seq_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#seq_choiceMixin"><span class="id" title="lemma">seq_choiceMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.OneType"><span class="id" title="section">OneType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="ChoiceTheory.TagChoice"><span class="id" title="section">TagChoice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="ChoiceTheory.TagChoice.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="ChoiceTheory.TagChoice.T_"><span class="id" title="variable">T_</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Fact</span> <a name="tagged_choiceMixin"><span class="id" title="lemma">tagged_choiceMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tagged_choiceType</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tagged_choiceMixin"><span class="id" title="lemma">tagged_choiceMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory.TagChoice"><span class="id" title="section">TagChoice</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fact</span> <a name="nat_choiceMixin"><span class="id" title="lemma">nat_choiceMixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">nat_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#nat_choiceMixin"><span class="id" title="lemma">nat_choiceMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="bool_choiceMixin"><span class="id" title="definition">bool_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#oddb"><span class="id" title="lemma">oddb</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bool_choiceMixin"><span class="id" title="definition">bool_choiceMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bitseq_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#bitseq"><span class="id" title="definition">bitseq</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="unit_choiceMixin"><span class="id" title="definition">unit_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bool_of_unitK"><span class="id" title="lemma">bool_of_unitK</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unit_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unit_choiceMixin"><span class="id" title="definition">unit_choiceMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="option_choiceMixin"><span class="id" title="definition">option_choiceMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#seq_of_optK"><span class="id" title="lemma">seq_of_optK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">option_choiceType</span> <span class="id" title="var">T</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#option_choiceMixin"><span class="id" title="definition">option_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sig_choiceMixin"><span class="id" title="definition">sig_choiceMixin</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a> :=<br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a> <span class="id" title="var">_</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sig_choiceType</span> <span class="id" title="var">T</span> (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#sig_choiceMixin"><span class="id" title="definition">sig_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="prod_choiceMixin"><span class="id" title="definition">prod_choiceMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanChoiceMixin"><span class="id" title="definition">CanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pairK"><span class="id" title="lemma">tag_of_pairK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">prod_choiceType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#prod_choiceMixin"><span class="id" title="definition">prod_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sum_choiceMixin"><span class="id" title="definition">sum_choiceMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#opair_of_sumK"><span class="id" title="lemma">opair_of_sumK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sum_choiceType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#sum_choiceMixin"><span class="id" title="definition">sum_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tree_choiceMixin"><span class="id" title="definition">tree_choiceMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#codeK"><span class="id" title="lemma">GenTree.codeK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tree_choiceType</span> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">GenTree.tree</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#tree_choiceMixin"><span class="id" title="definition">tree_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#ChoiceTheory"><span class="id" title="section">ChoiceTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">&quot;</span></a>[ 'choiceMixin' 'of' T 'by' &lt;: ]" :=<br/>
+&nbsp;&nbsp;(<a class="idref" href="mathcomp.ssreflect.choice.html#sub_choiceMixin"><span class="id" title="definition">sub_choiceMixin</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#choiceMixin"><span class="id" title="abbreviation">choiceMixin</span></a> <span class="id" title="var">T</span>)<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'choiceMixin'  'of'  T  'by'  &lt;: ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="Countable"><span class="id" title="module">Countable</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Record</span> <a name="Countable.mixin_of"><span class="id" title="record">mixin_of</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="Countable.Mixin"><span class="id" title="constructor">Mixin</span></a> {<br/>
+&nbsp;&nbsp;<a name="Countable.pickle"><span class="id" title="projection">pickle</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>;<br/>
+&nbsp;&nbsp;<a name="Countable.unpickle"><span class="id" title="projection">unpickle</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>;<br/>
+&nbsp;&nbsp;<a name="Countable.pickleK"><span class="id" title="projection">pickleK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="method">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="method">unpickle</span></a><br/>
+}.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.EqMixin"><span class="id" title="definition">EqMixin</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#PcanEqMixin"><span class="id" title="definition">PcanEqMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.pickleK"><span class="id" title="projection">pickleK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.ChoiceMixin"><span class="id" title="definition">ChoiceMixin</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanChoiceMixin"><span class="id" title="lemma">PcanChoiceMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.pickleK"><span class="id" title="projection">pickleK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Countable.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Record</span> <a name="Countable.class_of"><span class="id" title="record">class_of</span></a> <span class="id" title="var">T</span> := <a name="Countable.Class"><span class="id" title="constructor">Class</span></a> { <a name="Countable.base"><span class="id" title="projection">base</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class_of"><span class="id" title="record">Choice.class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>; <a name="Countable.mixin"><span class="id" title="projection">mixin</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a> }.<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="Countable.type"><span class="id" title="record">type</span></a> : <span class="id" title="keyword">Type</span> := <a name="Countable.Pack"><span class="id" title="constructor">Pack</span></a> {<a name="Countable.sort"><span class="id" title="projection">sort</span></a> : <span class="id" title="keyword">Type</span>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sort"><span class="id" title="method">sort</span></a>; <span class="id" title="var">_</span> : <span class="id" title="keyword">Type</span>}.<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Countable.ClassDef.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>) (<a name="Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.type"><span class="id" title="record">type</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.class"><span class="id" title="definition">class</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">_</span> <span class="id" title="var">c</span> <span class="id" title="var">_</span> <span class="id" title="keyword">as</span> <span class="id" title="var">cT'</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT'"><span class="id" title="variable">cT'</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">c</span>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">c</span> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Let</span> <a name="Countable.ClassDef.xT"><span class="id" title="variable">xT</span></a> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">T</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Countable.xclass"><span class="id" title="abbreviation">xclass</span></a> := (<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class"><span class="id" title="definition">class</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.class_of"><span class="id" title="record">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.xT"><span class="id" title="variable">xT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">m</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">bT</span> <span class="id" title="var">b</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.class"><span class="id" title="definition">Choice.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bT"><span class="id" title="variable">bT</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Pack"><span class="id" title="constructor">Pack</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Class"><span class="id" title="constructor">Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.eqType"><span class="id" title="definition">eqType</span></a> := @<a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Pack"><span class="id" title="constructor">Equality.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.xclass"><span class="id" title="abbreviation">xclass</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.xT"><span class="id" title="variable">xT</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Countable.choiceType"><span class="id" title="definition">choiceType</span></a> := @<a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Pack"><span class="id" title="constructor">Choice.Pack</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.xclass"><span class="id" title="abbreviation">xclass</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef.xT"><span class="id" title="variable">xT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ClassDef"><span class="id" title="section">ClassDef</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="Countable.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">base</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.base"><span class="id" title="projection">Choice.class_of</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">mixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">class_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.mixin"><span class="id" title="projection">mixin_of</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.sort"><span class="id" title="projection">Sortclass</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.eqType"><span class="id" title="definition">Equality.type</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">eqType</span>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.choiceType"><span class="id" title="definition">Choice.type</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">choiceType</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.type"><span class="id" title="record">type</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.pack"><span class="id" title="definition">pack</span></a> <span class="id" title="var">T</span> <span class="id" title="var">m</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>).<br/>
+<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Mixin"><span class="id" title="constructor">Mixin</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Countable.Exports.CountChoiceMixin"><span class="id" title="abbreviation">CountChoiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.ChoiceMixin"><span class="id" title="definition">ChoiceMixin</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="45eb30de99675fc3a25ff0fa8a76c46a"><span class="id" title="notation">&quot;</span></a>[ 'countType' 'of' T 'for' cT ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">cT</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#idfun"><span class="id" title="abbreviation">idfun</span></a>)<br/>
+&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'countType'  'of'  T  'for'  cT ]") : <span class="id" title="var">form_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">&quot;</span></a>[ 'countType' 'of' T ]" := (@<a class="idref" href="mathcomp.ssreflect.choice.html#Countable.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</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">format</span> "[ 'countType'  'of'  T ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable"><span class="id" title="module">Countable</span></a>.<br/>
+<span class="id" title="keyword">Export</span> <span class="id" title="var">Countable.Exports</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="unpickle"><span class="id" title="definition">unpickle</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="projection">Countable.unpickle</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#class"><span class="id" title="definition">Countable.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="pickle"><span class="id" title="definition">pickle</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="projection">Countable.pickle</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#class"><span class="id" title="definition">Countable.class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="CountableTheory"><span class="id" title="section">CountableTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="CountableTheory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pickleK"><span class="id" title="lemma">pickleK</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="pickle_inv"><span class="id" title="definition">pickle_inv</span></a> <span class="id" title="var">n</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#obind"><span class="id" title="abbreviation">obind</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pickle_invK"><span class="id" title="lemma">pickle_invK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#ocancel"><span class="id" title="definition">ocancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_inv"><span class="id" title="definition">pickle_inv</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pickleK_inv"><span class="id" title="lemma">pickleK_inv</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_inv"><span class="id" title="definition">pickle_inv</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pcan_pickleK"><span class="id" title="lemma">pcan_pickleK</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> :<br/>
+&nbsp;&nbsp;@<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcomp"><span class="id" title="definition">pcomp</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> (<span class="id" title="var">fK</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a>) :=<br/>
+&nbsp;&nbsp;@<a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.choice.html#pcan_pickleK"><span class="id" title="lemma">pcan_pickleK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fK"><span class="id" title="variable">fK</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> (<span class="id" title="var">fK</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#f'"><span class="id" title="variable">f'</span></a>) :=<br/>
+&nbsp;&nbsp;@<a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#can_pcan"><span class="id" title="lemma">can_pcan</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#fK"><span class="id" title="variable">fK</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sub_countMixin"><span class="id" title="definition">sub_countMixin</span></a> <span class="id" title="var">P</span> <span class="id" title="var">sT</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.eqtype.html#valK"><span class="id" title="lemma">valK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="pickle_seq"><span class="id" title="definition">pickle_seq</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#code"><span class="id" title="definition">CodeSeq.code</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="unpickle_seq"><span class="id" title="definition">unpickle_seq</span></a> <span class="id" title="var">n</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#pmap"><span class="id" title="definition">pmap</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#decode"><span class="id" title="definition">CodeSeq.decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#n"><span class="id" title="variable">n</span></a>)).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pickle_seqK"><span class="id" title="lemma">pickle_seqK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_seq"><span class="id" title="definition">pickle_seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle_seq"><span class="id" title="definition">unpickle_seq</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="seq_countMixin"><span class="id" title="definition">seq_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_seqK"><span class="id" title="lemma">pickle_seqK</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">seq_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.choice.html#seq_countMixin"><span class="id" title="definition">seq_countMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableTheory"><span class="id" title="section">CountableTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">&quot;</span></a>[ 'countMixin' 'of' T 'by' &lt;: ]" :=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.ssreflect.choice.html#sub_countMixin"><span class="id" title="definition">sub_countMixin</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#mixin_of"><span class="id" title="record">Countable.mixin_of</span></a> <span class="id" title="var">T</span>)<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'countMixin'  'of'  T  'by'  &lt;: ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="SubCountType"><span class="id" title="section">SubCountType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="SubCountType.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a name="SubCountType.P"><span class="id" title="variable">P</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">Countable</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="subCountType"><span class="id" title="record">subCountType</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
+&nbsp;&nbsp;<a name="SubCountType"><span class="id" title="constructor">SubCountType</span></a> {<a name="subCount_sort"><span class="id" title="projection">subCount_sort</span></a> :&gt; <a class="idref" href="mathcomp.ssreflect.eqtype.html#subType"><span class="id" title="record">subType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType.P"><span class="id" title="variable">P</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#subCount_sort"><span class="id" title="method">subCount_sort</span></a>}.<br/>
+
+<br/>
+<span class="id" title="keyword">Coercion</span> <span class="id" title="var">sub_countType</span> (<span class="id" title="var">sT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#subCountType"><span class="id" title="record">subCountType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#pack"><span class="id" title="definition">pack</span></a> (<span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType"><span class="id" title="constructor">SubCountType</span></a> <span class="id" title="var">_</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.choice.html#mixin_of"><span class="id" title="record">mixin_of</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">m</span>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sub_countType</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="pack_subCountType"><span class="id" title="definition">pack_subCountType</span></a> <span class="id" title="var">U</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">sT</span> <span class="id" title="var">cT</span> &amp; <a class="idref" href="mathcomp.ssreflect.eqtype.html#sub_sort"><span class="id" title="projection">sub_sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sort"><span class="id" title="projection">sort</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT"><span class="id" title="variable">cT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#U"><span class="id" title="variable">U</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> <span class="id" title="var">m</span>   &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#Class"><span class="id" title="constructor">Class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#class"><span class="id" title="definition">class</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#cT"><span class="id" title="variable">cT</span></a>) ⇒ @<a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType"><span class="id" title="constructor">SubCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#m"><span class="id" title="variable">m</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#SubCountType"><span class="id" title="section">SubCountType</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This assumes that T has both countType and subType structures.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Notation</span> <a name="8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">&quot;</span></a>[ 'subCountType' 'of' T ]" :=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;(@<a class="idref" href="mathcomp.ssreflect.choice.html#pack_subCountType"><span class="id" title="definition">pack_subCountType</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">T</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</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">format</span> "[ 'subCountType'  'of'  T ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="TagCountType"><span class="id" title="section">TagCountType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="TagCountType.I"><span class="id" title="variable">I</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>) (<a name="TagCountType.T_"><span class="id" title="variable">T_</span></a> : <a class="idref" href="mathcomp.ssreflect.choice.html#I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="pickle_tagged"><span class="id" title="definition">pickle_tagged</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">}</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#code"><span class="id" title="definition">CodeSeq.code</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#tag"><span class="id" title="definition">tag</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</span></a>)<a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle"><span class="id" title="definition">pickle</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#tagged"><span class="id" title="definition">tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#u"><span class="id" title="variable">u</span></a>)<a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="unpickle_tagged"><span class="id" title="definition">unpickle_tagged</span></a> <span class="id" title="var">s</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.choice.html#decode"><span class="id" title="definition">CodeSeq.decode</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">[::</span></a> <span class="id" title="var">ni</span><a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">;</span></a> <span class="id" title="var">nx</span><a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">]</span></a> <span class="id" title="keyword">then</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#obind"><span class="id" title="abbreviation">obind</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#omap"><span class="id" title="abbreviation">omap</span></a> (@<a class="idref" href="mathcomp.ssreflect.eqtype.html#Tagged"><span class="id" title="definition">Tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.I"><span class="id" title="variable">I</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.T_"><span class="id" title="variable">T_</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <span class="id" title="var">nx</span>)) (<a class="idref" href="mathcomp.ssreflect.choice.html#unpickle"><span class="id" title="definition">unpickle</span></a> <span class="id" title="var">ni</span>)<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pickle_taggedK"><span class="id" title="lemma">pickle_taggedK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_tagged"><span class="id" title="definition">pickle_tagged</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unpickle_tagged"><span class="id" title="definition">unpickle_tagged</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tag_countMixin"><span class="id" title="definition">tag_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#pickle_taggedK"><span class="id" title="lemma">pickle_taggedK</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tag_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.I"><span class="id" title="variable">I</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType.T_"><span class="id" title="variable">T_</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#50b5d8dd6be4fba768e35617e518ad76"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#tag_countMixin"><span class="id" title="definition">tag_countMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#TagCountType"><span class="id" title="section">TagCountType</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ The remaining Canonicals for standard datatypes.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Section</span> <a name="CountableDataTypes"><span class="id" title="section">CountableDataTypes</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#countType"><span class="id" title="abbreviation">countType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="nat_pickleK"><span class="id" title="lemma">nat_pickleK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#pcancel"><span class="id" title="definition">pcancel</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).  <br/>
+<span class="id" title="keyword">Definition</span> <a name="nat_countMixin"><span class="id" title="definition">nat_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountMixin"><span class="id" title="abbreviation">CountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#nat_pickleK"><span class="id" title="lemma">nat_pickleK</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">nat_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#nat_countMixin"><span class="id" title="definition">nat_countMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="bool_countMixin"><span class="id" title="definition">bool_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#oddb"><span class="id" title="lemma">oddb</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bool_countMixin"><span class="id" title="definition">bool_countMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bitseq_countType</span> :=  <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">countType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#bitseq"><span class="id" title="definition">bitseq</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="unit_countMixin"><span class="id" title="definition">unit_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#bool_of_unitK"><span class="id" title="lemma">bool_of_unitK</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">unit_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#unit_countMixin"><span class="id" title="definition">unit_countMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="option_countMixin"><span class="id" title="definition">option_countMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#seq_of_optK"><span class="id" title="lemma">seq_of_optK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">option_countType</span> <span class="id" title="var">T</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#option_countMixin"><span class="id" title="definition">option_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sig_countMixin"><span class="id" title="definition">sig_countMixin</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sig_countType</span> <span class="id" title="var">T</span> (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#sig_countMixin"><span class="id" title="definition">sig_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sig_subCountType</span> <span class="id" title="var">T</span> (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="prod_countMixin"><span class="id" title="definition">prod_countMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CanCountMixin"><span class="id" title="definition">CanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#tag_of_pairK"><span class="id" title="lemma">tag_of_pairK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">prod_countType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#prod_countMixin"><span class="id" title="definition">prod_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sum_countMixin"><span class="id" title="definition">sum_countMixin</span></a> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.choice.html#opair_of_sumK"><span class="id" title="lemma">opair_of_sumK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sum_countType</span> <span class="id" title="var">T1</span> <span class="id" title="var">T2</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#sum_countMixin"><span class="id" title="definition">sum_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T1"><span class="id" title="variable">T1</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T2"><span class="id" title="variable">T2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tree_countMixin"><span class="id" title="definition">tree_countMixin</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#PcanCountMixin"><span class="id" title="definition">PcanCountMixin</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#codeK"><span class="id" title="lemma">GenTree.codeK</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tree_countType</span> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.choice.html#tree"><span class="id" title="inductive">GenTree.tree</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.choice.html#tree_countMixin"><span class="id" title="definition">tree_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.choice.html#CountableDataTypes"><span class="id" title="section">CountableDataTypes</span></a>.<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
+\ No newline at end of file
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.choice.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)