Bijection, from very explicit to very implicit:
Bijection := '(f := _) -> '(a := _) -> '(b := _) -> '(n := _ : Nat) -> '(m := _ : Nat) -> '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(f) -> '(a) -> '(b) -> '(n : Nat) -> '(m : Nat) -> '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(f) -> '(a) -> '(b) -> '(n) -> '(m) -> '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(_ : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(_ : (_ :# n) -> (_ :# m)) -> '(n = m)
Bijection := '(_ : (_ :# n) -> (_ :# n)) -> '(n = n)
Bijection := '((_ :# n) -> (_ :# n)) -> '(n = n)