diff options
| -rw-r--r-- | hott/Identity.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index 571617a..b82c9c2 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -304,6 +304,8 @@ Lemma use_transport: shows "trans P p\<inverse> u: P y" by typechk +method transport uses eq = (rule use_transport[OF eq]) + Lemma (derive) transport_left_inv: assumes "A: U i" |