title: Proving `weaken` doesn't change the value of a number
body: <p>Let's say we want to prove that weakening the upper bound of a <code>Data.Fin</code> doesn't change the value of the number. The intuitive way to state this is:</p>
  
  <pre><code>weakenEq : (num : Fin n) -&gt; num = weaken num
  </code></pre>
  
  <p>Let's now generate the defini... Hold on! Let's think a bit about that statement. <code>num</code> and <code>weaken num</code> have different <em>types</em>. Can we state the equality in this case?</p>
  
  <p>The documentation on <code>=</code> suggests we can try to, but we might want to use <code>~=~</code> instead. Well, anyway, let's go ahead and generate the definition and case-split, resulting in</p>
  
  <pre><code>weakenEq : (num : Fin n) -&gt; num = weaken num
  weakenEq FZ = ?weakenEq_rhs_1
  weakenEq (FS x) = ?weakenEq_rhs_2
  </code></pre>
  
  <p>The goal in the <code>weakenEq_rhs_1</code> hole is <code>FZ = FZ</code>, which still makes sense from the value point of view. So we optimistically replace the hole with <code>Refl</code>, but only to fail:</p>
  
  <pre><code>When checking right hand side of weakenEq with expected type
          FZ = weaken FZ
  
  Unifying k and S k would lead to infinite value
  </code></pre>
  
  <p>A somewhat cryptic error message, so we wonder if that's really related to the types being different.</p>
  
  <p>Anyway, let's try again, but now with <code>~=~</code> instead of <code>=</code>. Unfortunately, the error is still the same.</p>
  
  <p>So, how one would state and prove that <code>weaken x</code> doesn't change the value of <code>x</code>? Does it really make sense to? What should I do if that's a part of a larger proof where I might want to <code>rewrite</code> a <code>Vect n (Fin k)</code> with <code>Vect n (Fin (S k))</code> that's obtained by <code>map</code>ping <code>weaken</code> over the original vector?</p>