<div dir="ltr">The K-rule is Streicher&#39;s axiom K.  A brief google search for &quot;axiom K&quot; gives me <a href="http://ncatlab.org/nlab/show/axiom+K">http://ncatlab.org/nlab/show/axiom+K</a> and <a href="http://adam.chlipala.net/cpdt/html/Equality.html">http://adam.chlipala.net/cpdt/html/Equality.html</a>.<div>

<br></div><div>-Jason</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, May 29, 2013 at 2:20 PM, Dmytro Starosud <span dir="ltr">&lt;<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Andrés/Everybody<br>
<br>
What does the K-rule mean?<br>
I cannot find any articles related to it in the internet.<br>
<br>
Thanks,<br>
Dmytro<br>
<br>
2013/5/29 Andrés Sicard-Ramírez &lt;<a href="mailto:andres.sicard.ramirez@gmail.com">andres.sicard.ramirez@gmail.com</a>&gt;:<br>
<div class="HOEnZb"><div class="h5">&gt; Hi,<br>
&gt;<br>
&gt; As far as I understand, the --without-K option rejects the K-rule which<br>
&gt; cannot be proved using subst. Given<br>
&gt;<br>
&gt; open import Data.List<br>
&gt; open import Data.Nat<br>
&gt; open import Data.Product<br>
&gt; open import Relation.Binary.PropositionalEquality<br>
&gt;<br>
&gt; open import Relation.Binary<br>
&gt; module NDTO = DecTotalOrder decTotalOrder<br>
&gt;<br>
&gt; P : {A : Set} → List A → List A → Set<br>
&gt; P xs ys = ∃ (λ x → ys ≡ x ∷ xs)<br>
&gt;<br>
&gt; Q : {A : Set} → List A → List A → Set<br>
&gt; Q xs ys = (length xs) &lt; (length ys)<br>
&gt;<br>
&gt; helper : {A : Set}(y : A)(xs : List A) → (length xs) &lt; (length (y ∷ xs))<br>
&gt; helper y []       = s≤s z≤n<br>
&gt; helper y (x ∷ xs) = s≤s NDTO.refl<br>
&gt;<br>
&gt; Why the --without-K option rejects the following proof<br>
&gt;<br>
&gt; foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys<br>
&gt; foo xs .(x ∷ xs) (x , refl) = helper x xs<br>
&gt;<br>
&gt; if I can prove foo using only subst<br>
&gt;<br>
&gt; foo&#39; : {A : Set}(xs ys : List A) → P xs ys → Q xs ys<br>
&gt; foo&#39; xs ys (x , h) =<br>
&gt;   subst (λ ys&#39; → length xs &lt; length ys&#39;) (sym h) (helper x xs)<br>
&gt;<br>
&gt; ?<br>
&gt;<br>
&gt; Thanks,<br>
&gt;<br>
&gt; --<br>
&gt; Andrés<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>