Set: pp::colors
  Set: pp::unicode
  Assumed: A
  Assumed: A'
  Assumed: B
  Assumed: B'
  Assumed: x
cast (Refl A) x
x == cast (Refl A) x
  Assumed: b
  Defined: f
  Assumed: H
  Assumed: a'
cast H (λ x : A, b) a'
  Assumed: H2
  Defined: g
0
g (cast H2 f a') : ℕ
cast H2 (λ x : A, b) a'
  Assumed: A1
  Assumed: A2
  Assumed: A3
  Assumed: Ha
  Assumed: Hb
  Assumed: a
cast Hb (cast Ha a)
cast Hb (cast Ha a) : A3