https://github.com/coq-ext-lib/coq-ext-lib
Tip revision: 4e16cb58bb743938ce27de4155ca97a43796db45 authored by Yishuai Li on 17 January 2024, 23:01:51 UTC
Update templates
Update templates
Tip revision: 4e16cb5
ExtLib.Data.SumN.html
<!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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="resources/config.js"></script>
<script type="text/javascript" src="resources/coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<h1 class="libtitle">ExtLib.Data.SumN</h1>
<div class="code">
<span class="id" title="var">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.PArith.PArith.html#"><span class="id" title="library">PArith</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#"><span class="id" title="library">ExtLib.Data.Map.FMapPositive</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Data.Eq.html#"><span class="id" title="library">ExtLib.Data.Eq</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Tactics.Injection.html#"><span class="id" title="library">ExtLib.Tactics.Injection</span></a>.<br/>
<span class="id" title="var">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.PArith.PArith.html#"><span class="id" title="library">PArith</span></a>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> (<span class="id" title="var">ts</span> : <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap"><span class="id" title="inductive">pmap</span></a> <span class="id" title="keyword">Type</span>) (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <span class="id" title="keyword">Type</span> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> => <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap_here"><span class="id" title="definition">pmap_here</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">p</span> => <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> (<a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap_right"><span class="id" title="definition">pmap_right</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a>) <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">p</span> => <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> (<a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap_left"><span class="id" title="definition">pmap_left</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a>) <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Record</span> <a name="OneOf"><span class="id" title="record">OneOf</span></a> (<span class="id" title="var">ts</span> : <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap"><span class="id" title="inductive">pmap</span></a> <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="mkOneOf"><span class="id" title="constructor">mkOneOf</span></a><br/>
{ <a name="index"><span class="id" title="projection">index</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a><br/>
; <a name="value"><span class="id" title="projection">value</span></a> : <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#index"><span class="id" title="method">index</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <span class="id" title="var">T</span><br/>
<span class="id" title="keyword">end</span><br/>
}.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Into"><span class="id" title="definition">Into</span></a> {<span class="id" title="var">ts</span>} {<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>} (<span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) (<span class="id" title="var">pf</span> : <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a>)<br/>
: <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pf"><span class="id" title="variable">pf</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">X</span> <span class="id" title="keyword">return</span> <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#X"><span class="id" title="variable">X</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a><br/>
<span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> => @<a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">mkOneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#n"><span class="id" title="variable">n</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="asNth'"><span class="id" title="definition">asNth'</span></a> {<span class="id" title="var">ts</span> : <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap"><span class="id" title="inductive">pmap</span></a> <span class="id" title="keyword">Type</span>} (<span class="id" title="var">p</span> <span class="id" title="var">p'</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>)<br/>
: <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p'"><span class="id" title="variable">p'</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <span class="id" title="var">T</span><br/>
<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <span class="id" title="var">T</span><br/>
<span class="id" title="keyword">end</span>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">as</span> <span class="id" title="var">p</span> , <a class="idref" href="ExtLib.Data.SumN.html#p'"><span class="id" title="variable">p'</span></a> <span class="id" title="keyword">as</span> <span class="id" title="var">p'</span><br/>
<span class="id" title="keyword">return</span> <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p'"><span class="id" title="variable">p'</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <span class="id" title="var">T</span><br/>
<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <span class="id" title="var">T</span><br/>
<span class="id" title="keyword">end</span>)<br/>
<span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> , <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">p</span> , <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">p'</span> => <a class="idref" href="ExtLib.Data.SumN.html#asNth'"><span class="id" title="definition">asNth'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p'"><span class="id" title="variable">p'</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">p</span> , <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">p'</span> => <a class="idref" href="ExtLib.Data.SumN.html#asNth'"><span class="id" title="definition">asNth'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p'"><span class="id" title="variable">p'</span></a><br/>
| <span class="id" title="var">_</span> , <span class="id" title="var">_</span> => <span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="asNth"><span class="id" title="definition">asNth</span></a> {<span class="id" title="var">ts</span> : <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap"><span class="id" title="inductive">pmap</span></a> <span class="id" title="keyword">Type</span>} (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) (<span class="id" title="var">oe</span> : <a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a>)<br/>
: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <span class="id" title="var">T</span><br/>
<span class="id" title="keyword">end</span>) :=<br/>
@<a class="idref" href="ExtLib.Data.SumN.html#asNth'"><span class="id" title="definition">asNth'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#oe"><span class="id" title="variable">oe</span></a>.(<a class="idref" href="ExtLib.Data.SumN.html#index"><span class="id" title="projection">index</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a>) <a class="idref" href="ExtLib.Data.SumN.html#oe"><span class="id" title="variable">oe</span></a>.(<a class="idref" href="ExtLib.Data.SumN.html#value"><span class="id" title="projection">value</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="OutOf"><span class="id" title="definition">OutOf</span></a> {<span class="id" title="var">ts</span>} {<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>} (<span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>)<br/>
(<span class="id" title="var">pf</span> : <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a>)<br/>
: <a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pf"><span class="id" title="variable">pf</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">X</span> <span class="id" title="keyword">return</span> <a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#X"><span class="id" title="variable">X</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a>:<span class="id" title="keyword">Type</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> => @<a class="idref" href="ExtLib.Data.SumN.html#asNth"><span class="id" title="definition">asNth</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#n"><span class="id" title="variable">n</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="asNth'_get_lookup"><span class="id" title="lemma">asNth'_get_lookup</span></a> : <span class="id" title="keyword">forall</span> <span class="id" title="var">p</span> <span class="id" title="var">ts</span> <span class="id" title="var">v</span>, <a class="idref" href="ExtLib.Data.SumN.html#asNth'"><span class="id" title="definition">asNth'</span></a> (<span class="id" title="var">ts</span>:=<a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a>) <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ExtLib.Data.SumN.html#v"><span class="id" title="variable">v</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">induction</span> <span class="id" title="var">p</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">intros</span>; <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Outof_Into"><span class="id" title="lemma">Outof_Into</span></a> : <span class="id" title="keyword">forall</span> <span class="id" title="var">ts</span> <span class="id" title="var">T</span> <span class="id" title="var">p</span> <span class="id" title="var">pf</span> <span class="id" title="var">v</span>,<br/>
@<a class="idref" href="ExtLib.Data.SumN.html#OutOf"><span class="id" title="definition">OutOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#pf"><span class="id" title="variable">pf</span></a> (@<a class="idref" href="ExtLib.Data.SumN.html#Into"><span class="id" title="definition">Into</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#pf"><span class="id" title="variable">pf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#v"><span class="id" title="variable">v</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ExtLib.Data.SumN.html#v"><span class="id" title="variable">v</span></a>.<br/>
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">using</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="ExtLib.Data.SumN.html#OutOf"><span class="id" title="definition">OutOf</span></a>, <a class="idref" href="ExtLib.Data.SumN.html#Into"><span class="id" title="definition">Into</span></a>.<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">repeat</span> <span class="id" title="tactic">rewrite</span> (<a class="idref" href="ExtLib.Data.Eq.html#eq_Arr_eq"><span class="id" title="lemma">eq_Arr_eq</span></a> <span class="id" title="var">pf</span>).<br/>
<span class="id" title="tactic">repeat</span> <span class="id" title="tactic">rewrite</span> (<a class="idref" href="ExtLib.Data.Eq.html#eq_Const_eq"><span class="id" title="lemma">eq_Const_eq</span></a> <span class="id" title="var">pf</span>).<br/>
<span class="id" title="tactic">repeat</span> <span class="id" title="tactic">rewrite</span> (<a class="idref" href="ExtLib.Data.Eq.html#eq_Const_eq"><span class="id" title="lemma">eq_Const_eq</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_sym"><span class="id" title="lemma">eq_sym</span></a> <span class="id" title="var">pf</span>)).<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="ExtLib.Data.SumN.html#asNth"><span class="id" title="definition">asNth</span></a>. <span class="id" title="tactic">simpl</span>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="ExtLib.Data.SumN.html#asNth'_get_lookup"><span class="id" title="lemma">asNth'_get_lookup</span></a>.<br/>
{ <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> (<a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <span class="id" title="var">ts</span> <span class="id" title="var">p</span>).<br/>
<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">reflexivity</span>. }<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="asNth_eq"><span class="id" title="lemma">asNth_eq</span></a><br/>
: <span class="id" title="keyword">forall</span> <span class="id" title="var">ts</span> <span class="id" title="var">p</span> <span class="id" title="var">oe</span> <span class="id" title="var">v</span>,<br/>
@<a class="idref" href="ExtLib.Data.SumN.html#asNth"><span class="id" title="definition">asNth</span></a> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#oe"><span class="id" title="variable">oe</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ExtLib.Data.SumN.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="ExtLib.Data.SumN.html#oe"><span class="id" title="variable">oe</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">{|</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">index</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">:=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">;</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">value</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">:=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">|}</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="ExtLib.Data.SumN.html#asNth"><span class="id" title="definition">asNth</span></a>.<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">oe</span>; <span class="id" title="tactic">simpl</span>.<br/>
<span class="id" title="var">revert</span> <span class="id" title="var">value0</span>. <span class="id" title="var">revert</span> <span class="id" title="var">index0</span>. <span class="id" title="var">revert</span> <span class="id" title="var">ts</span>.<br/>
<span class="id" title="tactic">induction</span> <span class="id" title="var">p</span>; <span class="id" title="tactic">destruct</span> <span class="id" title="var">index0</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">intros</span>;<br/>
<span class="id" title="tactic">solve</span> [ <span class="id" title="tactic">congruence</span> | <span class="id" title="tactic">eapply</span> <span class="id" title="var">IHp</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H</span> <span class="id" title="var">IHp</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">auto</span> ].<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="elim"><span class="id" title="section">elim</span></a>.<br/>
<span class="id" title="keyword">Context</span> {<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>}.<br/>
<span class="id" title="keyword">Variable</span> <a name="elim.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="ExtLib.Data.SumN.html#elim.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Type</span>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="pmap_elim"><span class="id" title="definition">pmap_elim</span></a> (<span class="id" title="var">R</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">ts</span> : <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap"><span class="id" title="inductive">pmap</span></a> <a class="idref" href="ExtLib.Data.SumN.html#elim.T"><span class="id" title="variable">T</span></a>) : <span class="id" title="keyword">Type</span> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#ts"><span class="id" title="variable">ts</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#Empty"><span class="id" title="constructor">Empty</span></a> => <a class="idref" href="ExtLib.Data.SumN.html#R"><span class="id" title="variable">R</span></a><br/>
| <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#Branch"><span class="id" title="constructor">Branch</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <span class="id" title="var">l</span> <span class="id" title="var">r</span> => <a class="idref" href="ExtLib.Data.SumN.html#pmap_elim"><span class="id" title="definition">pmap_elim</span></a> (<a class="idref" href="ExtLib.Data.SumN.html#pmap_elim"><span class="id" title="definition">pmap_elim</span></a> <a class="idref" href="ExtLib.Data.SumN.html#R"><span class="id" title="variable">R</span></a> <span class="id" title="var">r</span>) <span class="id" title="var">l</span><br/>
| <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#Branch"><span class="id" title="constructor">Branch</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span>) <span class="id" title="var">l</span> <span class="id" title="var">r</span> => <a class="idref" href="ExtLib.Data.SumN.html#elim.F"><span class="id" title="variable">F</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-></span></a> <a class="idref" href="ExtLib.Data.SumN.html#pmap_elim"><span class="id" title="definition">pmap_elim</span></a> (<a class="idref" href="ExtLib.Data.SumN.html#pmap_elim"><span class="id" title="definition">pmap_elim</span></a> <a class="idref" href="ExtLib.Data.SumN.html#R"><span class="id" title="variable">R</span></a> <span class="id" title="var">r</span>) <span class="id" title="var">l</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ExtLib.Data.SumN.html#elim"><span class="id" title="section">elim</span></a>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="pmap_lookup'_Empty"><span class="id" title="definition">pmap_lookup'_Empty</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) : <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#Empty"><span class="id" title="constructor">Empty</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">p</span> => <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'_Empty"><span class="id" title="definition">pmap_lookup'_Empty</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">p</span> => <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'_Empty"><span class="id" title="definition">pmap_lookup'_Empty</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="OneOf_Empty"><span class="id" title="definition">OneOf_Empty</span></a> (<span class="id" title="var">f</span> : <a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#Empty"><span class="id" title="constructor">Empty</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#False"><span class="id" title="inductive">False</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">f</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'_Empty"><span class="id" title="definition">pmap_lookup'_Empty</span></a> <span class="id" title="tactic">in</span> *.<br/>
<span class="id" title="tactic">intuition</span> <span class="id" title="tactic">congruence</span>.<br/>
<span class="id" title="keyword">Defined</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="pmap_lookup'_eq"><span class="id" title="lemma">pmap_lookup'_eq</span></a> <span class="id" title="var">p</span> <span class="id" title="var">m</span> : <a class="idref" href="ExtLib.Data.Map.FMapPositive.html#pmap_lookup"><span class="id" title="definition">pmap_lookup</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="ExtLib.Data.SumN.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <a class="idref" href="ExtLib.Data.SumN.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="ExtLib.Data.SumN.html#p"><span class="id" title="variable">p</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">m</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">p</span>; <span class="id" title="tactic">intuition</span>.<br/>
<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span>. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'_Empty"><span class="id" title="definition">pmap_lookup'_Empty</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> *. <span class="id" title="tactic">apply</span> <span class="id" title="var">IHp</span>.<br/>
<span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> *. <span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span>. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'_Empty"><span class="id" title="definition">pmap_lookup'_Empty</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">IHp</span>.<br/>
<span class="id" title="keyword">Defined</span>.<br/>
<br/>
<span class="id" title="keyword">Global Instance</span> <a name="Injective_OneOf"><span class="id" title="instance">Injective_OneOf</span></a> <span class="id" title="var">m</span> <span class="id" title="var">i1</span> <span class="id" title="var">i2</span> <span class="id" title="var">v1</span> <span class="id" title="var">v2</span><br/>
: <a class="idref" href="ExtLib.Tactics.Injection.html#Injective"><span class="id" title="class">Injective</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq"><span class="id" title="inductive">eq</span></a> (<a class="idref" href="ExtLib.Data.SumN.html#OneOf"><span class="id" title="record">OneOf</span></a> <a class="idref" href="ExtLib.Data.SumN.html#m"><span class="id" title="variable">m</span></a>)<br/>
{| <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">index</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">:=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">i1</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">;</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">value</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">:=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">v1</span></a> |}<br/>
{| <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">index</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">:=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">i2</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">;</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">value</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">:=</span></a> <a class="idref" href="ExtLib.Data.SumN.html#mkOneOf"><span class="id" title="constructor">v2</span></a> |}) :=<br/>
{ <a class="idref" href="ExtLib.Tactics.Injection.html#result"><span class="id" title="method">result</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <span class="id" title="var">pf</span> : <span class="id" title="var">i2</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">i1</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
<span class="id" title="var">v1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pf"><span class="id" title="variable">pf</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">T</span> <span class="id" title="keyword">return</span> <span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <span class="id" title="var">m</span> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> => <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a><br/>
<span class="id" title="keyword">end</span> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> => <span class="id" title="var">v2</span><br/>
<span class="id" title="keyword">end</span><br/>
; <a class="idref" href="ExtLib.Tactics.Injection.html#injection"><span class="id" title="method">injection</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <span class="id" title="var">H</span> =><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#H"><span class="id" title="variable">H</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">h</span><br/>
<span class="id" title="keyword">return</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <span class="id" title="var">pf</span> : <a class="idref" href="ExtLib.Data.SumN.html#index"><span class="id" title="projection">index</span></a> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Data.SumN.html#h"><span class="id" title="variable">h</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">i1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
<span class="id" title="var">v1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="keyword">match</span><br/>
<a class="idref" href="ExtLib.Data.SumN.html#pf"><span class="id" title="variable">pf</span></a> <span class="id" title="tactic">in</span> (<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">T</span>)<br/>
<span class="id" title="keyword">return</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ExtLib.Data.SumN.html#pmap_lookup'"><span class="id" title="definition">pmap_lookup'</span></a> <span class="id" title="var">m</span> <a class="idref" href="ExtLib.Data.SumN.html#T"><span class="id" title="variable">T</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T0</span> => <span class="id" title="var">T0</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Datatypes.html#Empty_set"><span class="id" title="inductive">Empty_set</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> => <a class="idref" href="ExtLib.Data.SumN.html#value"><span class="id" title="projection">value</span></a> <span class="id" title="var">_</span> <a class="idref" href="ExtLib.Data.SumN.html#h"><span class="id" title="variable">h</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> => @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#ex_intro"><span class="id" title="constructor">ex_intro</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#eq_refl"><span class="id" title="constructor">eq_refl</span></a><br/>
<span class="id" title="keyword">end</span><br/>
}.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
