lean2/tests/lean/elab5.lean.expected.out
Leonardo de Moura b7b868de85 fix(library/elaborator): bug reported by Jeremy Avigad
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-10 14:01:22 -08:00

20 lines
700 B
Text

Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
Set: lean::pp::implicit
import "kernel"
import "Nat"
variable C {A B : Type} (H : @eq Type A B) (a : A) : B
variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (∀ x : A, B x) (∀ x : A', B' x)) :
@eq Type A A'
variable R {A A' : Type}
{B : A → Type}
{B' : A' → Type}
(H : @eq Type (∀ x : A, B x) (∀ x : A', B' x))
(a : A) :
@eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
@R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a