2b2aa228e3
The universe constraint manager is more flexible now. We don't need to start with a huge universe U >= 512. We can start small, and increase it on demand. If module mod1 needs it, it can always add universe U >= 3 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
33 lines
973 B
Text
33 lines
973 B
Text
Set: pp::colors
|
|
Set: pp::unicode
|
|
Imported 'cast'
|
|
Set: pp::colors
|
|
Defined: TypeM
|
|
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
|
|
∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
|
|
λ (A A' : TypeM)
|
|
(B : A → TypeM)
|
|
(B' : A' → TypeM)
|
|
(f : ∀ x : A, B x)
|
|
(g : ∀ x : A', B' x)
|
|
(a : A)
|
|
(b : A')
|
|
(H1 : (∀ x : A, B x) == (∀ x : A', B' x))
|
|
(H2 : f == g)
|
|
(H3 : a == b),
|
|
let L1 : A == A' := dominj H1,
|
|
L2 : A' == A := symm L1,
|
|
b' : A := cast L2 b,
|
|
L3 : b == b' := cast::eq L2 b,
|
|
L4 : a == b' := htrans H3 L3,
|
|
L5 : f a == f b' := congr2 f L4
|
|
in L5 :
|
|
∀ (A A' : TypeM)
|
|
(B : A → TypeM)
|
|
(B' : A' → TypeM)
|
|
(f : ∀ x : A, B x)
|
|
(g : ∀ x : A', B' x)
|
|
(a : A)
|
|
(b : A')
|
|
(H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
|
|
f == g → a == b → f a == f (cast (symm (dominj H1)) b)
|