2013-09-06 18:31:47 -07:00
|
|
|
Set: pp::colors
|
|
|
|
Set: pp::unicode
|
2013-12-23 22:04:19 -08:00
|
|
|
Assumed: cast
|
|
|
|
Assumed: CastEq
|
|
|
|
Assumed: CastApp
|
|
|
|
Assumed: DomInj
|
|
|
|
Assumed: RanInj
|
2013-09-06 18:31:47 -07:00
|
|
|
Assumed: A
|
|
|
|
Assumed: B
|
|
|
|
Assumed: A'
|
|
|
|
Assumed: B'
|
|
|
|
Assumed: H
|
|
|
|
Assumed: a
|
2013-10-29 16:20:02 -07:00
|
|
|
DomInj H : A == A'
|
2013-09-06 18:31:47 -07:00
|
|
|
Proved: BeqB'
|
|
|
|
Set: lean::pp::implicit
|
2013-12-21 17:02:16 -08:00
|
|
|
@DomInj A A' (λ x : A, B) (λ x : A', B') H
|
|
|
|
@RanInj A A' (λ x : A, B) (λ x : A', B') H a
|