diff options
| author | Josh Chen | 2021-04-17 17:41:56 +0100 |
|---|---|---|
| committer | Josh Chen | 2021-04-17 17:41:56 +0100 |
| commit | 75ab44cc1d2ad63864ecb43215a56538748fc0d3 (patch) | |
| tree | 58e3b532fd01502b4c2fa9bf237a3b0970b16e57 /hott/Identity.thy | |
| parent | 54df7336797dfa07124652a9eb75aac978a1a359 (diff) | |
| parent | 092875d160a2d18c94bde41c6472e8031ab57313 (diff) | |
Merge branch 'dev'
Diffstat (limited to '')
| -rw-r--r-- | hott/Identity.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index 0531b74..9ae0894 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -244,7 +244,7 @@ Lemma (def) ap_funcomp: "p: x = y" shows "(g \<circ> f)[p] = g[f[p]]" apply (eq p) - \<^item> by compute + \<^item> by (subst comp; typechk?)+ \<^item> by compute refl done |