diff options
| author | Josh Chen | 2021-04-17 17:16:45 +0100 |
|---|---|---|
| committer | Josh Chen | 2021-04-17 17:16:45 +0100 |
| commit | 3a34ca2b43fbd5725a7435dfafdb4cf179a8ec8b (patch) | |
| tree | e2dc28dce94c43f545fdce472b82a2c77256964a /mltt | |
| parent | d379e77dab3ff6a854b94af47be6098a2ba6ca64 (diff) | |
Small fix: extraneous variable
Diffstat (limited to 'mltt')
| -rw-r--r-- | mltt/core/MLTT.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy index 18bd2b7..19b9563 100644 --- a/mltt/core/MLTT.thy +++ b/mltt/core/MLTT.thy @@ -443,7 +443,7 @@ Lemma funcomp_lambda_comp [comp]: Lemma funcomp_apply_comp [comp]: assumes - "A: U i" "B: U i" "\<And>x y. x: B \<Longrightarrow> C x: U i" + "A: U i" "B: U i" "\<And>x. x: B \<Longrightarrow> C x: U i" "f: A \<rightarrow> B" "g: \<Prod>x: B. C x" "x: A" shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)" |