auto gitdoc commit
This commit is contained in:
parent
9617c7ae9b
commit
4ecd3f7c93
1 changed files with 3 additions and 1 deletions
|
@ -390,7 +390,9 @@ theorem2∙13∙1 m n = encode m n , equiv
|
|||
|
||||
c : (x : ℕ) → decode x x (r x) ≡ refl
|
||||
c zero = refl
|
||||
c (suc x) = {! !}
|
||||
c (suc x) =
|
||||
let wtf = c x in
|
||||
{! !}
|
||||
|
||||
equiv = record
|
||||
{ g = decode m n
|
||||
|
|
Loading…
Reference in a new issue