lean2/tests/lean/tst4.lean.expected.out

  Set: pp::colors
  Set: pp::unicode
  Assumed: f
  Assumed: N
  Assumed: n1
  Assumed: n2
  Set: lean::pp::implicit
f::explicit N n1 n2
f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
  Assumed: EqNice
EqNice::explicit N n1 n2
N
Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
f::explicit N n1 n2
  Assumed: a
  Assumed: b
  Assumed: c
  Assumed: g
  Assumed: H1
  Proved: Pr
Axiom H1 : a = b ∧ b = c
Theorem Pr : (g a) = (g c) :=
    let κ::1 := Trans::explicit
                     N
                     a
                     b
                     c
                     (Conjunct1::explicit (a = b) (b = c) H1)
                     (Conjunct2::explicit (a = b) (b = c) H1)
    in Congr::explicit N (λ x : N, N) g g a c (Refl::explicit (N → N) g) κ::1