auto gitdoc commit
This commit is contained in:
parent
5ed0e3ac96
commit
c0222459c3
1 changed files with 3 additions and 2 deletions
|
@ -414,8 +414,9 @@ theorem2∙13∙1 m n = encode m n , equiv
|
|||
|
||||
-- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c
|
||||
res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c
|
||||
res = {! !}
|
||||
in res
|
||||
res = {! !}
|
||||
|
||||
in {! !}
|
||||
|
||||
equiv = record
|
||||
{ g = decode m n
|
||||
|
|
Loading…
Reference in a new issue