lean2/tests/lean/elab5.lean
Leonardo de Moura 57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00

12 lines
498 B
Text

variable C {A B : Type} (H : A = B) (a : A) : B
variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B x) = (forall x : A', B' x)) : A = A'
variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B x) = (forall x : A', B' x)) (a : A) :
(B a) = (B' (C (D H) a))
theorem R2 : forall (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) :=
fun A1 A2 B1 B2 H a, R H a
set_option pp::implicit true
print environment 7.